map_sSup — Mathlib

English

If f is normal and s is a nonempty small set of ordinals, f(sSup s) = sSup (f '' s).

Русский

Если f нормальная и s непустое малое множество ординалов, тогда f( sSup s ) = sSup( f '' s ).

LaTeX

$$$$ f\\left( \\operatorname{sSup} s \\right) = \\operatorname{Sups}(f'' s) $$$$

Lean4

theorem map_sSup {f : Ordinal.{u} → Ordinal.{v}} (H : IsNormal f) {s : Set Ordinal.{u}} (hn : s.Nonempty)
    [Small.{u} s] : f (sSup s) = sSup (f '' s) :=
  H.map_sSup_of_bddAbove (bddAbove_of_small s) hn

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