csInf_lt_iff — Mathlib

English

If s is bounded below and nonempty, then sInf s < a iff there exists b ∈ s with b < a.

Русский

Если s ограничено снизу и непусто, то sInf s < a эквивалентно существованию b ∈ s such that b < a.

LaTeX

$$$ (hb : BddBelow s) \land (hs : s.Nonempty) \\Rightarrow (sInf s < a \iff \exists b \in s, b < a)$$$

Lean4

theorem csInf_lt_iff (hb : BddBelow s) (hs : s.Nonempty) : sInf s < a ↔ ∃ b ∈ s, b < a :=
  isGLB_lt_iff <| isGLB_csInf hs hb

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