ι : Type u_1
I J : Box ι
x y l u : ι → ℝ
⊢ (if h : ∀ (i : ι), l i < u i then ↑{ lower := l, upper := u, lower_lt_upper := h } else ⊥) = ⊥ ↔ ∃ i, u i ≤ l i
ι : Type u_1
I J : Box ι
x y l u : ι → ℝ
⊢ mk' l u = ⊥ ↔ ∃ i, u i ≤ l i
rw [mk']
no goals
ι : Type u_1
I J : Box ι
x y l u : ι → ℝ
⊢ (if h : ∀ (i : ι), l i < u i then ↑{ lower := l, upper := u, lower_lt_upper := h } else ⊥) = ⊥ ↔ ∃ i, u i ≤ l i
split_ifs with h <;> simpa using h