English
Let s be a set bounded above, and let a ∈ s and b ∈ α satisfy b < a. Then b is strictly less than the supremum of s; i.e., b < sSup(s).
Русский
Пусть s — множество, ограниченное сверху, и пусть a ∈ s и b ∈ α удовлетворяют b < a. Тогда b строго меньше наибольшей верхней границы множества s; то есть b < sSup(s).
LaTeX
$$$\forall \alpha\, [\text{ConditionallyCompleteLattice } \alpha]\; \forall s : \text{Set }\alpha\, \forall a,b : \alpha,\ BddAbove\ s \to a \in s \to b < a \to b < \operatorname{sSup} s$$$
Lean4
/-- `b < sSup s` when there is an element `a` in `s` with `b < a`, when `s` is bounded above.
This is essentially an iff, except that the assumptions for the two implications are
slightly different (one needs boundedness above for one direction, nonemptiness and linear
order for the other one), so we formulate separately the two implications, contrary to
the `CompleteLattice` case. -/
theorem lt_csSup_of_lt (hs : BddAbove s) (ha : a ∈ s) (h : b < a) : b < sSup s :=
lt_of_lt_of_le h (le_csSup hs ha)
