le_csInf_iff' — Mathlib

English

For a nonempty s, b ≤ sInf s iff b is a lower bound of s; equivalently, sInf s is the greatest lower bound.

Русский

Для непустого s, b ≤ sInf s эквивалентно тому, что b является нижней гранью s; инфimum — наибольшая нижняя грань.

LaTeX

$$$ (hs : s.Nonempty) : b \le sInf s \iff b \in lowerBounds s $$$

Lean4

theorem le_csInf_iff' (hs : s.Nonempty) : b ≤ sInf s ↔ b ∈ lowerBounds s :=
  le_isGLB_iff (isLeast_csInf hs).isGLB

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