English
Let α be a ConditionallyCompleteLattice and b ∈ α. Let f : ι → α be a function indexed by a nonempty set ι. If f(i) ≤ b for all i and every w < b is strictly below some f(i), then the supremum of the family {f(i)} is b.
Русский
Пусть α — частично упорядоченная неполная решетка с условной полнотой, и задана функция f: ι → α над непустым индексовым множеством ι. Если f(i) ≤ b для всех i и для каждого w < b существует i, такой что w < f(i), то верхняя грань множества {f(i)} равна b.
LaTeX
$$$\text{If }(\forall i, f(i) \le b) \ \text{and } (\forall w, w < b \rightarrow \exists i, w < f(i)), \text{ then } \sup_{i} f(i) = b.$$$
Lean4
/-- Introduction rule to prove that `b` is the supremum of `f`: it suffices to check that `b`
is larger than `f i` for all `i`, and that this is not the case of any `w<b`.
See `iSup_eq_of_forall_le_of_forall_lt_exists_gt` for a version in complete lattices. -/
theorem ciSup_eq_of_forall_le_of_forall_lt_exists_gt [Nonempty ι] {f : ι → α} (h₁ : ∀ i, f i ≤ b)
(h₂ : ∀ w, w < b → ∃ i, w < f i) : ⨆ i : ι, f i = b :=
csSup_eq_of_forall_le_of_forall_lt_exists_gt (range_nonempty f) (forall_mem_range.mpr h₁) fun w hw =>
exists_range_iff.mpr <| h₂ w hw
