fp_iff_deriv

Mathlib.SetTheory.Ordinal.FixedPoint

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

English

For a normal f, f a = a iff there exists o with deriv f o = a.

Русский

Для нормальной f, f a = a тогда и только если существует o, такой что deriv f o = a.

LaTeX

$$$$ f a = a \iff \exists o, \operatorname{deriv} f o = a $$$$

Lean4

theorem fp_iff_deriv (H : IsNormal f) {a} : f a = a ↔ ∃ o, deriv f o = a := by rw [← H.le_iff_eq, H.le_iff_deriv]

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

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

Разделы

Аффилиация

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