map_sSup_of_bddAbove — Mathlib

English

If f is normal, for a bounded nonempty set s of ordinals, f(sSup s) equals sSup of f '' s.

Русский

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

LaTeX

$$$$ f\\left( \\operatorname{sSup}(s) \\right) = \\operatorname{Sups}(f\\,'' s) \\quad\\text{for } hs, hn: BddAbove(s), s.Nonempty. $$$$

Lean4

theorem map_sSup_of_bddAbove {f : Ordinal.{u} → Ordinal.{v}} (H : IsNormal f) {s : Set Ordinal.{u}} (hs : BddAbove s)
    (hn : s.Nonempty) : f (sSup s) = sSup (f '' s) :=
  by
  have := hn.to_subtype
  rw [sSup_eq_iSup', sSup_image', H.map_iSup_of_bddAbove]
  rwa [Subtype.range_coe_subtype, setOf_mem_eq]

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