nfp_le

Mathlib.SetTheory.Ordinal.FixedPoint

URI: https://scilib.ai/kg/mathlib#Ordinal.nfp_le

English

For any f and a, b, (nfp f a ≤ b) iff (∀ n, f^[n] a ≤ b).

Русский

Для любых f, a, b: nfp f a ≤ b эквивалентно ∀ n, f^[n] a ≤ b.

LaTeX

$$$$ (nfp f a \le b) \iff (\forall n, f^{[n]} a \le b). $$$$

Lean4

theorem nfp_le {a b} : (∀ n, f^[n] a ≤ b) → nfp f a ≤ b :=
  nfp_le_iff.2

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

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

Разделы

Аффилиация

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