English
Let s be a subset of a complete lattice and b ∈ α. If ∀ a ∈ s, a ≤ b and ∀ w < b there exists a ∈ s with w < a, then sSup s = b.
Русский
Пусть s ⊆ α и b ∈ α. Если ∀ a ∈ s, a ≤ b и ∀ w < b существует a ∈ s с w < a, то sSup s = b.
LaTeX
$$$$ \Big( \forall a \in s,\ a \le b \Bigr) \rightarrow \Big( \forall w,\ w < b \rightarrow \exists a \in s,\ w < a \Big) \rightarrow \operatorname{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 `csSup_eq_of_forall_le_of_forall_lt_exists_gt` for a version in conditionally complete
lattices. -/
theorem sSup_eq_of_forall_le_of_forall_lt_exists_gt (h₁ : ∀ a ∈ s, a ≤ b) (h₂ : ∀ w, w < b → ∃ a ∈ s, w < a) :
sSup s = b :=
(sSup_le h₁).eq_of_not_lt fun h =>
let ⟨_, ha, ha'⟩ := h₂ _ h
((le_sSup ha).trans_lt ha').false
