exists_eq_iSup_of_not_isSuccPrelimit

English

If IsLUB (range f) x and ¬IsPredPrelimit x, then ∃ i, f(i) = x.

Русский

Если x является наименьшей верхней гранью диапазона и x не пред предел, тогда существует i, такое что f(i) = x.

LaTeX

$$$ IsLUB (range f) x \\land \\neg IsPredPrelimit x \\Rightarrow \\exists i\\, f(i) = x $$$

Lean4

theorem exists_eq_iSup_of_not_isSuccPrelimit (hf : ¬IsSuccPrelimit (⨆ i, f i)) : ∃ i, f i = ⨆ i, f i :=
  sSup_mem_of_not_isSuccPrelimit hf

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