lift_ofNat

Mathlib.SetTheory.Cardinal.Order

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

English

For n with AtLeastTwo, lift(ofNat(n)) = OfNat.ofNat(n).

Русский

Для n с условием AtLeastTwo выполняется lift(ofNat(n)) = OfNat.ofNat(n).

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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