English
Let s be a nonempty subset of a ConditionallyComplete lattice. If b is an upper bound for s and every upper bound ub of s satisfies b ≤ ub, then sSup s = b.
Русский
Пусть s — непустое подмножество условно полной решетки. Если b является верхней гранью для s и для любой верхней грани ub выполняется b ≤ ub, то sSup s = b.
LaTeX
$$$ \text{hs : } s \neq \varnothing \, \land \, (\forall a \in s, a \le b) \, \land \, (\forall ub, (\forall a \in s, a \le ub) \rightarrow b \le ub) \Rightarrow sSup s = b $$$
Lean4
/-- Introduction rule to prove that `b` is the supremum of `s`: it suffices to check that
1) `b` is an upper bound
2) every other upper bound `b'` satisfies `b ≤ b'`. -/
theorem csSup_eq_of_is_forall_le_of_forall_le_imp_ge (hs : s.Nonempty) (h_is_ub : ∀ a ∈ s, a ≤ b)
(h_b_le_ub : ∀ ub, (∀ a ∈ s, a ≤ ub) → b ≤ ub) : sSup s = b :=
(csSup_le hs h_is_ub).antisymm ((h_b_le_ub _) fun _ => le_csSup ⟨b, h_is_ub⟩)
