nfp_le_apply

Mathlib.SetTheory.Ordinal.FixedPoint

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

English

For a normal f, the comparison f b ≤ nfp f a is equivalent to b ≤ nfp f a.

Русский

Для нормальной f сравнение f b ≤ nfp f a эквивалентно b ≤ nfp f a.

LaTeX

$$$$ (f b \le nfp f a) \iff (b \le nfp f a). $$$$

Lean4

theorem nfp_le_apply (H : IsNormal f) {a b} : nfp f a ≤ f b ↔ nfp f a ≤ b :=
  le_iff_le_iff_lt_iff_lt.2 H.apply_lt_nfp

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

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

Разделы

Аффилиация

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