nfp_fp

Mathlib.SetTheory.Ordinal.FixedPoint

URI: https://scilib.ai/kg/mathlib#Ordinal.IsNormal.nfp_fp

English

For a normal f, for every a, f(nfp f a) = nfp f a.

Русский

Для нормальной f для каждого a выполняется f(nfp f a) = nfp f a.

LaTeX

$$$$ f(\operatorname{nfp} f a) = \operatorname{nfp} f a. $$$$

Lean4

theorem nfp_fp (H : IsNormal f) : ∀ a, f (nfp f a) = nfp f a :=
  @nfpFamily_fp Unit (fun _ => f) _ () H

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru