one_add_ofNat

Mathlib.SetTheory.Ordinal.Arithmetic

URI: https://scilib.ai/kg/mathlib#Ordinal.one_add_ofNat

English

For any natural m, 1 + ofNat(m) equals succ(ofNat(m)).

Русский

Для любого натурального m, 1 + ofNat(m) равно succ(ofNat(m)).

LaTeX

$$$1 + (\operatorname{ofNat}(m)) = \operatorname{succ}(\operatorname{ofNat}(m))$$$

Lean4

@[simp]
theorem one_add_ofNat (m : ℕ) [m.AtLeastTwo] : 1 + (ofNat(m) : Ordinal) = Order.succ (OfNat.ofNat m : Ordinal) :=
  one_add_natCast m

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

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

Разделы

Аффилиация

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