ι : Type u_1
I✝ J I : Box ι
s t : Set ι
h : s ≠ t
⊢ ↑(splitCenterBox I s) ⊓ ↑(splitCenterBox I t) ≤ ⊥
ι : Type u_1
I✝ J I : Box ι
s t : Set ι
h : s ≠ t
⊢ Disjoint ↑(splitCenterBox I s) ↑(splitCenterBox I t)
rw [disjoint_iff_inf_le]
case intro
ι : Type u_1
I✝ J I : Box ι
s t : Set ι
h : s ≠ t
y : ι → ℝ
hs : y ∈ ↑(splitCenterBox I s)
ht : y ∈ ↑(splitCenterBox I t)
⊢ y ∈ ⊥
ι : Type u_1
I✝ J I : Box ι
s t : Set ι
h : s ≠ t
⊢ ↑(splitCenterBox I s) ⊓ ↑(splitCenterBox I t) ≤ ⊥
rintro y ⟨hs, ht⟩
case intro
ι : Type u_1
I✝ J I : Box ι
s t : Set ι
h : s ≠ t
y : ι → ℝ
hs : y ∈ ↑(splitCenterBox I s)
ht : y ∈ ↑(splitCenterBox I t)
⊢ s = t
case intro
ι : Type u_1
I✝ J I : Box ι
s t : Set ι
h : s ≠ t
y : ι → ℝ
hs : y ∈ ↑(splitCenterBox I s)
ht : y ∈ ↑(splitCenterBox I t)
⊢ y ∈ ⊥
apply h
case intro.h
ι : Type u_1
I✝ J I : Box ι
s t : Set ι
h : s ≠ t
y : ι → ℝ
hs : y ∈ ↑(splitCenterBox I s)
ht : y ∈ ↑(splitCenterBox I t)
i : ι
⊢ i ∈ s ↔ i ∈ t
case intro
ι : Type u_1
I✝ J I : Box ι
s t : Set ι
h : s ≠ t
y : ι → ℝ
hs : y ∈ ↑(splitCenterBox I s)
ht : y ∈ ↑(splitCenterBox I t)
⊢ s = t
ext i
case intro.h
ι : Type u_1
I✝ J I : Box ι
s t : Set ι
h : s ≠ t
y : ι → ℝ
hs : y ∈ I ∧ ∀ (i : ι), (lower I i + upper I i) / 2 < y i ↔ i ∈ s
ht : y ∈ I ∧ ∀ (i : ι), (lower I i + upper I i) / 2 < y i ↔ i ∈ t
i : ι
⊢ i ∈ s ↔ i ∈ t
case intro.h
ι : Type u_1
I✝ J I : Box ι
s t : Set ι
h : s ≠ t
y : ι → ℝ
hs : y ∈ ↑(splitCenterBox I s)
ht : y ∈ ↑(splitCenterBox I t)
i : ι
⊢ i ∈ s ↔ i ∈ t
rw [mem_coe, mem_splitCenterBox] at hs ht
no goals
case intro.h
ι : Type u_1
I✝ J I : Box ι
s t : Set ι
h : s ≠ t
y : ι → ℝ
hs : y ∈ I ∧ ∀ (i : ι), (lower I i + upper I i) / 2 < y i ↔ i ∈ s
ht : y ∈ I ∧ ∀ (i : ι), (lower I i + upper I i) / 2 < y i ↔ i ∈ t
i : ι
⊢ i ∈ s ↔ i ∈ t
rw [← hs.2, ← ht.2]