iSup_coe_lt_top — Mathlib

English

The iSup over the casts is less than top exactly when the range is bounded above: ⨆ i (f i : ℕ∞) < ⊤ ↔ BddAbove (range f).

Русский

iSup над отображениями меньше ⊤ тогда и только тогда, когда множество значений ограничено сверху.

LaTeX

$$$$ \\langle \\mathrm{iSup}_{i} (f(i)^{\\ cast}) \\rangle < \\top \\iff \\mathrm{BddAbove}(\\mathrm{range}(f)) $$$$

Lean4

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

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