zero_left

Mathlib.SetTheory.Ordinal.CantorNormalForm

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

English

CNF.zero_left expresses that if o ≠ 0, CNF(0, o) is the list with a single pair (0, o).

Русский

CNF.zero_left выражает, что если o ≠ 0, CNF(0, o) задается как единичный элемент (0, o).

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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