le_csInf_iff — Mathlib

English

For a nonempty s bounded below, a ≤ sInf s iff ∀ b ∈ s, a ≤ b.

Русский

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

LaTeX

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

Lean4

theorem le_csInf_iff (hb : BddBelow s) (hs : s.Nonempty) : a ≤ sInf s ↔ ∀ b ∈ s, a ≤ b :=
  le_isGLB_iff (isGLB_csInf hs hb)

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