ι : Type u_1
M : Type ?u.3630
n : ℕ
I : Box ι
i✝ : ι
x✝ : ℝ
y : ι → ℝ
i : ι
x : ℝ
⊢ (min x (upper I i) ≤ lower I i ∨ ∃ x x_1, upper I x ≤ lower I x) ↔ x ≤ lower I i
ι : Type u_1
M : Type ?u.3630
n : ℕ
I : Box ι
i✝ : ι
x✝ : ℝ
y : ι → ℝ
i : ι
x : ℝ
⊢ splitLower I i x = ⊥ ↔ x ≤ lower I i
rw [splitLower, mk'_eq_bot, exists_update_iff I.upper fun j y => y ≤ I.lower j]
no goals
ι : Type u_1
M : Type ?u.3630
n : ℕ
I : Box ι
i✝ : ι
x✝ : ℝ
y : ι → ℝ
i : ι
x : ℝ
⊢ (min x (upper I i) ≤ lower I i ∨ ∃ x x_1, upper I x ≤ lower I x) ↔ x ≤ lower I i
simp [(I.lower_lt_upper _).not_le]