ciInf_eq_top_of_top_mem — Mathlib

English

Let α be a conditionally complete linear order with top ⊤. If there exists i such that f(i) = ⊤, then iSup f = ⊤.

Русский

Пусть α — условно полноупорядоченный линейный порядок с вершиной ⊤. Если существует индекс i с f(i) = ⊤, то наибольшая верхняя грань iSup f равна ⊤.

LaTeX

$$$ \top \in \mathrm{range}(f) \Rightarrow \sup_{i \in ι} f(i) = \top $$$

Lean4

theorem ciInf_eq_top_of_top_mem [OrderTop α] {f : ι → α} (hs : ⊤ ∈ range f) : iSup f = ⊤ :=
  csSup_eq_top_of_top_mem hs

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