English
Let b ∈ α and f : ι → α. If ∀ i, f(i) ≤ b and ∀ w < b, ∃ i, w < f(i), then ⨆ i, f(i) = b.
Русский
Пусть b ∈ α и f : ι → α. Если ∀ i, f(i) ≤ b и ∀ w < b существует i, such that w < f(i), тогда ⨆ i, f(i) = b.
LaTeX
$$$$\left( \forall i, f(i) \le b \right) \rightarrow \left( \forall w, w < b \rightarrow \exists i, w < f(i) \right) \rightarrow \bigvee_{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 `ciSup_eq_of_forall_le_of_forall_lt_exists_gt` for a version in conditionally complete
lattices. -/
theorem iSup_eq_of_forall_le_of_forall_lt_exists_gt {f : ι → α} (h₁ : ∀ i, f i ≤ b) (h₂ : ∀ w, w < b → ∃ i, w < f i) :
⨆ i : ι, f i = b :=
sSup_eq_of_forall_le_of_forall_lt_exists_gt (forall_mem_range.mpr h₁) fun w hw => exists_range_iff.mpr <| h₂ w hw
