map_iSup_of_bddAbove — Mathlib

English

If f is normal and g is a function with range bounded above, then applying f to the supremum of g equals the supremum of f composed with g.

Русский

Пусть f нормальная, и g имеет ограниченную верхнюю границу область значений. Тогда f( sup_i g(i) ) = sup_i f(g(i)).

LaTeX

$$$$ f\\left( \\bigvee_{i} g(i) \\right) = \\bigvee_{i} f(g(i)) \\quad\\text{provided } BddAbove(\\operatorname{range}(g)). $$$$

Lean4

theorem map_iSup_of_bddAbove {f : Ordinal.{u} → Ordinal.{v}} (H : IsNormal f) {ι : Type*} (g : ι → Ordinal.{u})
    (hg : BddAbove (range g)) [Nonempty ι] : f (⨆ i, g i) = ⨆ i, f (g i) :=
  Order.IsNormal.map_iSup H hg

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