exists_eq_natCast_of_iSup_eq — Mathlib

English

Let f: ι → Cardinal with bounded range and ⨆ i, f(i) = n for some natural n. Then there exists i with f(i) = n.

Русский

Пусть f: ι → кардиналы с ограниченным диапазоном и ⨆ i, f(i) = n для некоторого n ∈ ℕ. Тогда существует i, такой что f(i) = n.

LaTeX

$$$ \sup_{i} f(i) = n \Rightarrow \exists i, f(i) = n $$$

Lean4

theorem exists_eq_natCast_of_iSup_eq {ι : Type u} [Nonempty ι] (f : ι → Cardinal.{v}) (hf : BddAbove (range f)) (n : ℕ)
    (h : ⨆ i, f i = n) : ∃ i, f i = n :=
  exists_eq_of_iSup_eq_of_not_isSuccLimit.{u, v} f hf (not_isSuccLimit_natCast n) h

Похожие утверждения