csInf_le_iff — Mathlib

English

For a nonempty s bounded below in α, sInf(s) ≤ a iff every lower bound of s is ≤ a.

Русский

Для непустого s, ограниченного снизу, в α верно: sInf(s) ≤ a тогда и только тогда, когда каждый нижний предел s ≤ a.

LaTeX

$$$BddBelow(s) \land s \neq \varnothing \rightarrow (sInf(s) \le a \iff \forall b (b \in \text{lowerBounds}(s) \rightarrow b \le a))$$$

Lean4

theorem csInf_le_iff (h : BddBelow s) (hs : s.Nonempty) : sInf s ≤ a ↔ ∀ b ∈ lowerBounds s, b ≤ a :=
  ⟨fun h _ hb => le_trans (le_csInf hs hb) h, fun hb => hb _ fun _ => csInf_le h⟩

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