nfp_le_of_principal

Mathlib.SetTheory.Ordinal.Principal

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

← MathLib Explorer

English

If a < o and o is principal, then nfp(op a) a ≤ o.

Русский

Если a < o и o — principal, то nfp(op a) a ≤ o.

LaTeX

$$$$ \forall {a o},\ \operatorname{Ordinal.partialOrder}.lt a o \Rightarrow \operatorname{Principal}(op)\ o \Rightarrow \operatorname{nfp}(\operatorname{op} a)\ a \le o. $$$$

Lean4

theorem nfp_le_of_principal (hao : a < o) (ho : Principal op o) : nfp (op a) a ≤ o :=
  nfp_le fun n => (ho.iterate_lt hao n).le

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

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

Разделы

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

Аффилиация

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