case h
ι : Type u_1
I✝ J I : Box ι
x : ι → ℝ
⊢ (x ∈ ⋃ (s : Set ι), ↑(splitCenterBox I s)) ↔ x ∈ ↑I
ι : Type u_1
I✝ J I : Box ι
⊢ (⋃ (s : Set ι), ↑(splitCenterBox I s)) = ↑I
ext x
no goals
case h
ι : Type u_1
I✝ J I : Box ι
x : ι → ℝ
⊢ (x ∈ ⋃ (s : Set ι), ↑(splitCenterBox I s)) ↔ x ∈ ↑I
simp