ι : Type u_1
I✝ J✝ : Box ι
x y : ι → ℝ
I J : WithBot (Box ι)
⊢ ↑I ⊓ ↑J ≤ ⊥ ↔ ↑I ∩ ↑J ⊆ ↑⊥
ι : Type u_1
I✝ J✝ : Box ι
x y : ι → ℝ
I J : WithBot (Box ι)
⊢ Disjoint ↑I ↑J ↔ Disjoint I J
simp only [disjoint_iff_inf_le, ← withBotCoe_subset_iff, coe_inf]
no goals
ι : Type u_1
I✝ J✝ : Box ι
x y : ι → ℝ
I J : WithBot (Box ι)
⊢ ↑I ⊓ ↑J ≤ ⊥ ↔ ↑I ∩ ↑J ⊆ ↑⊥
rfl