one_left

Mathlib.SetTheory.Ordinal.CantorNormalForm

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

English

CNF.one_left asserts that if o ≠ 0, CNF(1, o) = [(0, o)].

Русский

CNF.one_left утверждает, что если o ≠ 0, CNF(1, o) = [(0, o)].

LaTeX

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

Lean4

protected theorem one_left {o : Ordinal} (ho : o ≠ 0) : CNF 1 o = [(0, o)] := by simp [CNF.ne_zero ho]

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

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

Разделы

Аффилиация

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