iSup_coe_ne_top — Mathlib

English

The negation of top for iSup is equivalent to boundedness: ⨆ i (f i : ℕ∞) ≠ ⊤ iff BddAbove (range f).

Русский

Неравенство верхней границы эквивалентно ограниченности: ⨆ i (f i) ≠ ⊤ ⇔ BddAbove (range f).

LaTeX

$$$$ \\big( \\big( \\mathrm{iSup}_{i} (f(i)) \\big)^{\\;cast} \\neq \\top \\big) \\iff \\mathrm{BddAbove}(\\mathrm{range}(f)) $$$$

Lean4

theorem iSup_coe_ne_top : ⨆ i, (f i : ℕ∞) ≠ ⊤ ↔ BddAbove (range f) :=
  iSup_coe_eq_top.not_left

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