nfpFamily_eq_self — Mathlib

English

If for every i, f_i a = a, then nfpFamily f a = a.

Русский

Если для каждого i выполняется f_i(a) = a, то nfpFamily f a = a.

LaTeX

$$$[Small.{u} ι] {a} (h : \\forall i, f i a = a) : nfpFamily f a = a$$

Lean4

theorem nfpFamily_eq_self [Small.{u} ι] {a} (h : ∀ i, f i a = a) : nfpFamily f a = a :=
  by
  apply (Ordinal.iSup_le ?_).antisymm (le_nfpFamily f a)
  intro l
  rw [List.foldr_fixed' h l]
    -- Todo: This is actually a special case of the fact the intersection of club sets is a club set.

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