sInf_le_iff — Mathlib

English

If s is bounded below, then sInf s ≤ a iff for all ε>0 there exists x ∈ s with x < a + ε.

Русский

Если s ограничено снизу, то sInf s ≤ a эквивалентно тому, что для каждого ε>0 существует x ∈ s такой, что x < a + ε.

LaTeX

$$$(h : BddBelow s) (h' : s.Nonempty) : sInf s \le a \iff \forall \epsilon>0, \exists x \in s, x < a + \epsilon$$$

Lean4

theorem sInf_le_iff (h : BddBelow s) (h' : s.Nonempty) : sInf s ≤ a ↔ ∀ ε, 0 < ε → ∃ x ∈ s, x < a + ε :=
  by
  rw [le_iff_forall_pos_lt_add]
  constructor <;> intro H ε ε_pos
  · exact exists_lt_of_csInf_lt h' (H ε ε_pos)
  · rcases H ε ε_pos with ⟨x, x_in, hx⟩
    exact csInf_lt_of_lt h x_in hx

Похожие утверждения