English
Let ι be nonempty and suppose ⨆ i, f i < ⊤. Then there exists i with f i = ⨆ i, f i.
Русский
Пусть ι непуст и предположим, что ⨆ i, f i < ⊤. Тогда существует i такое, что f i = ⨆ i, f i.
LaTeX
$$$(\text{Nonempty } \iota) \;\land\; (\sup_i f i) < \top \;\Rightarrow\; \exists i, f(i) = \sup_i f i$$$
Lean4
theorem sSup_eq_top_of_infinite (h : s.Infinite) : sSup s = ⊤ :=
by
apply (sSup_eq_top ..).mpr
intro x hx
cases x with
| top => simp at hx
| coe x =>
contrapose! h
simp only [not_infinite]
apply Finite.subset <| Finite.Set.finite_image {n : ℕ | n ≤ x} (fun (n : ℕ) => (n : ℕ∞))
intro y hy
specialize h y hy
have hxt : y < ⊤ := lt_of_le_of_lt h hx
use y.toNat
simp [toNat_le_of_le_coe h, LT.lt.ne_top hxt]
