English
If s is bounded below, a ∈ s and a < b, then the infimum of s lies strictly below b; i.e., sInf s < b.
Русский
Если s ограничено снизу, a ∈ s и a < b, тогда infimum множества s лежит строго ниже b; то есть sInf s < b.
LaTeX
$$$\forall \alpha\, [\text{ConditionallyCompleteLattice } \alpha] \; {s : \text{Set }\alpha} \; {a,b : \alpha},\ BddBelow\ s \to a \in s \to a < b \to sInf\ s < b$$$
Lean4
/-- `sInf s < b` when there is an element `a` in `s` with `a < b`, when `s` is bounded below.
This is essentially an iff, except that the assumptions for the two implications are
slightly different (one needs boundedness below for one direction, nonemptiness and linear
order for the other one), so we formulate separately the two implications, contrary to
the `CompleteLattice` case. -/
theorem csInf_lt_of_lt : BddBelow s → a ∈ s → a < b → sInf s < b :=
lt_csSup_of_lt (α := αᵒᵈ)
