exists_eq_of_iSup_eq_of_not_isSuccLimit

English

If ω is not a succ-limit and the iSup of f equals ω, then there exists i with f(i) = ω.

Русский

Если ω не является succ-пределом, и iSup f = ω, то существует i, такой что f(i) = ω.

LaTeX

$$∃ i, f i = ω$$

Lean4

theorem exists_eq_of_iSup_eq_of_not_isSuccLimit {ι : Type u} [hι : Nonempty ι] (f : ι → Cardinal.{v})
    (hf : BddAbove (range f)) {c : Cardinal.{v}} (hc : ¬IsSuccLimit c) (h : ⨆ i, f i = c) : ∃ i, f i = c :=
  by
  rw [Cardinal.isSuccLimit_iff] at hc
  refine
    (not_and_or.mp hc).elim (fun e ↦ ⟨hι.some, ?_⟩) (Cardinal.exists_eq_of_iSup_eq_of_not_isSuccPrelimit.{u, v} f c · h)
  cases not_not.mp e
  rw [← le_zero_iff] at h ⊢
  exact (le_ciSup hf _).trans h

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