English
A constructive criterion: if s is nonempty, every a ∈ s is ≤ b, and every w < b has some a ∈ s with w < a, then sSup s = b.
Русский
Конструктивная характеристика: если s непусто, каждый элемент ≤ b и для любого w < b существует a ∈ s такой, что w < a, тогда sSup s = b.
LaTeX
$$$s.NE \neq \varnothing \rightarrow (\forall a \in s, a \le b) \rightarrow (\forall w, w < b \rightarrow \exists a \in s, w < a) \rightarrow \mathrm{sSup}(s) = b$$$
Lean4
/-- Introduction rule to prove that `b` is the supremum of `s`: it suffices to check that `b`
is larger than all elements of `s`, and that this is not the case of any `w<b`.
See `sSup_eq_of_forall_le_of_forall_lt_exists_gt` for a version in complete lattices. -/
theorem csSup_eq_of_forall_le_of_forall_lt_exists_gt (hs : s.Nonempty) (H : ∀ a ∈ s, a ≤ b)
(H' : ∀ w, w < b → ∃ a ∈ s, w < a) : sSup s = b :=
(eq_of_le_of_not_lt (csSup_le hs H)) fun hb =>
let ⟨_, ha, ha'⟩ := H' _ hb
lt_irrefl _ <| ha'.trans_le <| le_csSup ⟨b, H⟩ ha
