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