exists_eq_of_iSup_eq_of_not_isSuccPrelimit

English

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

Русский

Если iSup f = ω и ω не является succ-prelimit, то существует i, для которого f(i) = ω.

LaTeX

$$∃ i, f i = ω$$

Lean4

theorem exists_eq_of_iSup_eq_of_not_isSuccPrelimit {ι : Type u} (f : ι → Cardinal.{v}) (ω : Cardinal.{v})
    (hω : ¬IsSuccPrelimit ω) (h : ⨆ i : ι, f i = ω) : ∃ i, f i = ω :=
  by
  subst h
  suffices BddAbove (range f) from (isLUB_csSup' this).mem_of_not_isSuccPrelimit hω
  contrapose! hω with hf
  rw [iSup, csSup_of_not_bddAbove hf, csSup_empty]
  exact isSuccPrelimit_bot

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