exists_eq_ciSup_of_not_isSuccPrelimit'

English

Let hf be BddAbove (range f) and hf' not IsSuccPrelimit (⨆ i, f i). Then ∃ i, f i = ⨆ i, f i.

Русский

Пусть hf — ограничено сверху (range f) и hf' не является IsSuccPrelimit для ⨆ i, f i. Тогда существует i, такое что f i = ⨆ i, f i.

LaTeX

$$$ BddAbove (range f) \\land \\neg IsSuccPrelimit (\\sup_i f(i)) \\Rightarrow \\exists i\, f(i) = \\sup_i f(i) $$$

Lean4

/-- See `exists_eq_ciSup_of_not_isSuccPrelimit` for the
`ConditionallyCompleteLinearOrder` version. -/
theorem exists_eq_ciSup_of_not_isSuccPrelimit' (hf : BddAbove (range f)) (hf' : ¬IsSuccPrelimit (⨆ i, f i)) :
    ∃ i, f i = ⨆ i, f i :=
  csSup_mem_of_not_isSuccPrelimit' hf hf'

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