exists_eq_ciSup_of_not_isSuccPrelimit

English

Let α be a conditionally complete linear order and f: ι → α with range f bounded above. If ⨆ i, f(i) is not a succ-prelimit, then there exists i with f(i) = ⨆ i, f(i).

Русский

Пусть α — условно полноупорядоченный линейный порядок и f: ι → α так, что множество значений f ограничено сверху. Если верхняя грань множества значений не является пред-предельным пределом, существует индекс i, для которого f(i) достигает этой верхней грани.

LaTeX

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

Lean4

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 (range_nonempty f) hf hf'

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