coeff_one_left

Mathlib.SetTheory.Ordinal.CantorNormalForm

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

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem coeff_one_left (o : Ordinal) : coeff 1 o = single 0 o :=
  coeff_of_le_one le_rfl o

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

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

Разделы

Аффилиация

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