coe_iSup — Mathlib

English

Let f : ι → ℕ. If the range of f is bounded above, then the coercion of the supremum to ENat equals the supremum of the coerced values, i.e., ↑(⨆ i, f i) = ⨆ i, (f i : ℕ∞).

Русский

Пусть f : ι → ℕ. Если образ f ограничен сверху, то приведение верхнего предела к ENat даёт верхний предел по приведённым значениям: ↑(⨆ i, f i) = ⨆ i, (f i : ℕ∞).

LaTeX

$$$\uparrow(\bigl(\bigvee_i f(i)\bigr)) = \bigvee_i (f(i) : \mathbb{N}_\infty)$$$

Lean4

theorem coe_iSup : BddAbove (range f) → ↑(⨆ i, f i) = ⨆ i, (f i : ℕ∞) :=
  WithTop.coe_iSup _

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