exists_lt_of_csInf_lt — Mathlib

English

In a linear order, if s is nonempty and sInf s < b, then there exists a ∈ s with a < b.

Русский

В линейном порядке, если s непусто и sInf s < b, найдется a ∈ s такое, что a < b.

LaTeX

$$$ (s \neq \varnothing) \land (sInf s < b) \Rightarrow \exists a \in s, a < b $$$

Lean4

/-- When `sInf s < b`, there is an element `a` in `s` with `a < b`, if `s` is nonempty and the order
is a linear order. -/
theorem exists_lt_of_csInf_lt (hs : s.Nonempty) (hb : sInf s < b) : ∃ a ∈ s, a < b :=
  exists_lt_of_lt_csSup (α := αᵒᵈ) hs hb

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