nfpFamily_fp — Mathlib

English

If H i: IsNormal (f i) for a given i and a, then f i(nfpFamily f a) = nfpFamily f a.

Русский

Для конкретного i, если f_i нормальна, то f_i( nfpFamily f a ) = nfpFamily f a.

LaTeX

$$$[Small.{u} ι] {i} (H : IsNormal (f i)) (a) : f i (nfpFamily f a) = nfpFamily f a$$

Lean4

theorem nfpFamily_fp [Small.{u} ι] {i} (H : IsNormal (f i)) (a) : f i (nfpFamily f a) = nfpFamily f a :=
  by
  rw [nfpFamily, H.map_iSup]
  apply le_antisymm <;> refine Ordinal.iSup_le fun l => ?_
  · exact Ordinal.le_iSup _ (i :: l)
  · exact H.le_apply.trans (Ordinal.le_iSup _ _)

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