isNormal_derivFamily — Mathlib

English

If each f_i is a normal function, then the derivative family derivFamily f is a normal function.

Русский

Если каждая функция f_i нормальная, то производная семейства derivFamily f является нормальной функцией.

LaTeX

$$$$ IsNormal(derivFamily f). $$$$

Lean4

theorem isNormal_derivFamily [Small.{u} ι] (f : ι → Ordinal.{u} → Ordinal.{u}) : IsNormal (derivFamily f) :=
  by
  refine IsNormal.of_succ_lt (fun o ↦ ?_) @fun o h ↦ ?_
  · rw [derivFamily_succ, ← succ_le_iff]
    exact le_nfpFamily _ _
  · rw [derivFamily_limit _ h, Set.image_eq_range]
    have := h.nonempty_Iio.to_subtype
    exact isLUB_ciSup (bddAbove_of_small _)

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