coeff_zero_left

Mathlib.SetTheory.Ordinal.CantorNormalForm

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

English

The coefficient function at base 0, for any o, is the singleton mapping o ↦ 0: coeff 0 o = single 0 o.

Русский

Коэффициентная функция при базe 0 равна единственному элементу: coeff 0 o = single 0 o.

LaTeX

$$$$ \\forall o:\\; \\operatorname{coeff}(0,o) = \\operatorname{single}(0)\\, o $$$$

Lean4

@[simp]
theorem coeff_zero_left (o : Ordinal) : coeff 0 o = single 0 o :=
  coeff_of_le_one zero_le_one o

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

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

Разделы

Аффилиация

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