English
If s is bounded above and nonempty, then a ≤ sSup s iff for all ε>0 there exists x ∈ s with a + ε > x.
Русский
Если s ограничено сверху и непусто, то a ≤ sSup s эквивалентно тому, что для всех ε>0 существует x ∈ s, такой что a + ε > x.
LaTeX
$$$(h : BddAbove s) (h' : s.Nonempty) : a \le sSup s \iff \forall \epsilon>0, \exists x \in s, a + \epsilon > x$$$
Lean4
theorem le_sSup_iff (h : BddAbove s) (h' : s.Nonempty) : a ≤ sSup s ↔ ∀ ε, ε < 0 → ∃ x ∈ s, a + ε < x :=
by
rw [le_iff_forall_pos_lt_add]
refine ⟨fun H ε ε_neg => ?_, fun H ε ε_pos => ?_⟩
· exact exists_lt_of_lt_csSup h' (lt_sub_iff_add_lt.mp (H _ (neg_pos.mpr ε_neg)))
· rcases H _ (neg_lt_zero.mpr ε_pos) with ⟨x, x_in, hx⟩
exact sub_lt_iff_lt_add.mp (lt_csSup_of_lt h x_in hx)
