isNormal_preOmega — Mathlib

English

preOmega is a normal function (strictly increasing and continuous at limits).

Русский

preOmega является нормальной функцией (строго возрастает и непрерывна на предельных точках).

LaTeX

$$$\mathrm{IsNormal}(\mathrm{preOmega})$$$

Lean4

theorem isNormal_preOmega : IsNormal preOmega :=
  by
  rw [isNormal_iff_strictMono_limit]
  refine
    ⟨preOmega_strictMono, fun o ho a ha ↦
      (preOmega_le_of_forall_lt (isInitial_ord _) fun b hb ↦ ?_).trans (ord_card_le a)⟩
  rw [← (isInitial_ord _).card_lt_card, card_ord]
  apply lt_of_lt_of_le _ (card_le_card <| ha _ (ho.succ_lt hb))
  rw [(isInitial_preOmega _).card_lt_card, preOmega_lt_preOmega]
  exact lt_succ b

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