sSup_ord — Mathlib

English

For f : ι → Cardinal, the ordinal of the supremum equals the supremum of the ordinals of f(i).

Русский

Для f : ι → Cardinal ординал верхней границы равен supremum ординалов f(i).

LaTeX

$$$$ (\\sup_{i} f(i)).\\operatorname{ord} = \\sup_{i} (f(i).\\operatorname{ord}) $$$$

Lean4

theorem sSup_ord (s : Set Cardinal) : (sSup s).ord = sSup (ord '' s) :=
  by
  obtain rfl | hn := s.eq_empty_or_nonempty
  · simp
  · by_cases hs : BddAbove s
    · exact isNormal_ord.map_sSup hn hs
    · rw [csSup_of_not_bddAbove hs, csSup_of_not_bddAbove (bddAbove_ord_image_iff.not.2 hs)]
      simp

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