of_lt

Mathlib.SetTheory.Ordinal.CantorNormalForm

URI: https://scilib.ai/kg/mathlib#Ordinal.CNF.of_lt

← MathLib Explorer

English

If o ≠ 0 and o < b, then CNF(b, o) = [(0, o)].

Русский

Если o ≠ 0 и o < b, тогда CNF(b, o) = [(0, o)].

LaTeX

$$$\forall b\,\forall o\; (o \neq 0) \land o < b \Rightarrow CNF(b, o) = [(0, o)]$$$

Lean4

protected theorem of_lt {b o : Ordinal} (ho : o ≠ 0) (hb : o < b) : CNF b o = [(0, o)] := by
  rw [CNF.ne_zero ho, log_eq_zero hb, opow_zero, div_one, mod_one, zero_right]

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

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

Разделы

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

Аффилиация

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