zero_right

Mathlib.SetTheory.Ordinal.CantorNormalForm

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

English

If o ≠ 0, then CNF(b, o) = [(0, o)] when o is less than b (i.e., in the simple left case).

Русский

Если o ≠ 0, то CNF(b, o) = [(0, o)] когда o меньше b, что соответствует простому левому случаю.

LaTeX

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

Lean4

@[simp]
theorem zero_right (b : Ordinal) : CNF b 0 = [] :=
  rec_zero b _ _

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

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

Разделы

Аффилиация

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