apply_lt_nfp

Mathlib.SetTheory.Ordinal.FixedPoint

URI: https://scilib.ai/kg/mathlib#Ordinal.IsNormal.apply_lt_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 < nfp f a) \iff (b < nfp f a). $$$$

Lean4

theorem apply_lt_nfp (H : IsNormal f) {a b} : f b < nfp f a ↔ b < nfp f a :=
  by
  unfold nfp
  rw [← @apply_lt_nfpFamily_iff Unit (fun _ => f) _ _ (fun _ => H) a b]
  exact ⟨fun h _ => h, fun h => h Unit.unit⟩

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

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

Разделы

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

Аффилиация

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