exists_isLeast_of_nonempty — Mathlib

English

Dually, if S is bounded below, there exists a least element of S.

Русский

Двойственно: если S ограничено снизу, существует наименьший элемент S.

LaTeX

$$$ \text{BddBelow}(S) \land S \neq \emptyset \Rightarrow \exists x, IsLeast(S,x).$$$

Lean4

theorem exists_isLeast_of_nonempty {X : Type*} [LinearOrder X] [PredOrder X] [IsPredArchimedean X] {S : Set X}
    (hS : BddBelow S) (hS' : S.Nonempty) : ∃ x, IsLeast S x :=
  hS.dual.exists_isGreatest_of_nonempty hS'

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