apply_le_nfp

Mathlib.SetTheory.Ordinal.FixedPoint

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

← MathLib Explorer

English

For a normal f, f b ≤ nfp f a iff 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 apply_le_nfp (H : IsNormal f) {a b} : f b ≤ nfp f a ↔ b ≤ nfp f a :=
  ⟨H.le_apply.trans, fun h => by simpa only [H.nfp_fp] using H.le_iff.2 h⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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