lift_eq_ofNat_iff

Mathlib.SetTheory.Cardinal.Order

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

English

lift(a) equals ofNat(n) iff a equals OfNat.ofNat(n).

Русский

lift(a) равно ofNat(n) тогда и только тогда, когда a равно OfNat.ofNat(n).

LaTeX

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

Lean4

@[simp]
theorem lift_eq_ofNat_iff {a : Cardinal.{u}} {n : ℕ} [n.AtLeastTwo] : lift.{v} a = ofNat(n) ↔ a = OfNat.ofNat n :=
  lift_eq_nat_iff

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

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

Разделы

Аффилиация

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