lift_ofNat

Mathlib.SetTheory.Ordinal.Arithmetic

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

English

Lifting the natural embedding of n equals its OfNat representation.

Русский

Поднятие враждебного встраивания n сопоставляется с OfNat(n).

LaTeX

$$$\mathrm{lift}(\operatorname{ofNat}(n)) = \operatorname{OfNat}.ofNat(n)$$$

Lean4

@[simp]
theorem lift_ofNat (n : ℕ) [n.AtLeastTwo] : lift.{u, v} ofNat(n) = OfNat.ofNat n :=
  lift_natCast n

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

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

Разделы

Аффилиация

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