iSup_coe_eq_top — Mathlib

English

For a family f: ι → Nat, the iSup over ENat-casts equals ⊤ if and only if not all elements are bounded above; i.e., not bounded above means the supremum is top.

Русский

Для f: ι → Nat верхняя грань достигается, если и только если множество значений не ограничено сверху; тогда iSup равно ⊤.

LaTeX

$$$$ \\operatorname{iSup}_{i} (f(i))^{\\ cast} = \\top \\iff \\neg \\mathrm{BddAbove}(\\mathrm{range}(f)) $$$$

Lean4

theorem iSup_coe_eq_top : ⨆ i, (f i : ℕ∞) = ⊤ ↔ ¬BddAbove (range f) :=
  WithTop.iSup_coe_eq_top

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