ext
R : Type u_1
inst✝⁵ : RealScalar R
W : Type ?u.9501
inst✝⁴ : SemiHilbert R W
X : Type ?u.9531
inst✝³ : SemiHilbert R X
Y : Type ?u.9555
inst✝² : SemiHilbert R Y
Z : Type ?u.9579
inst✝¹ : SemiHilbert R Z
inst✝ : MeasureSpace R
height x : R
⊢ (fun z => (x, z)) ⁻¹' {(x, z) | 1 ≤ x ∧ x ≤ height ∧ 0 ≤ z ∧ z ≤ x} = if x ∈ Icc 1 height then Icc 0 x else ∅
case h
R : Type u_1
inst✝⁵ : RealScalar R
W : Type ?u.9501
inst✝⁴ : SemiHilbert R W
X : Type ?u.9531
inst✝³ : SemiHilbert R X
Y : Type ?u.9555
inst✝² : SemiHilbert R Y
Z : Type ?u.9579
inst✝¹ : SemiHilbert R Z
inst✝ : MeasureSpace R
height x x✝ : R
⊢ x✝ ∈ (fun z => (x, z)) ⁻¹' {(x, z) | 1 ≤ x ∧ x ≤ height ∧ 0 ≤ z ∧ z ≤ x} ↔
    x✝ ∈ if x ∈ Icc 1 height then Icc 0 x else ∅