map_iSup — Mathlib

English

For a normal function f and a family g of ordinals, the supremum commutes with f without any boundedness assumption, provided index set is Small.

Русский

Для нормальной функции f и семейства g пределов. Supremum коммутирует с f при условии, что индексное множество малого размера.

LaTeX

$$$$ f\\left( \\bigvee_{i} g(i) \\right) = \\bigvee_{i} f(g(i)) $$$$

Lean4

theorem map_iSup {f : Ordinal.{u} → Ordinal.{v}} (H : IsNormal f) {ι : Type w} (g : ι → Ordinal.{u}) [Small.{u} ι]
    [Nonempty ι] : f (⨆ i, g i) = ⨆ i, f (g i) :=
  H.map_iSup_of_bddAbove g (bddAbove_of_small _)

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