ofNat_eq_lift_iff

Mathlib.SetTheory.Cardinal.Order

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

← MathLib Explorer

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 ofNat_eq_lift_iff {a : Cardinal.{u}} {n : ℕ} [n.AtLeastTwo] :
    (ofNat(n) : Cardinal) = lift.{v} a ↔ (OfNat.ofNat n : Cardinal) = a :=
  nat_eq_lift_iff

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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