ofENat_eq_ofNat

Mathlib.SetTheory.Cardinal.ENat

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

English

For m ∈ ENat and n ∈ ℕ with [n.AtLeastTwo], (m : Cardinal) = ofNat n ↔ m = OfNat.ofNat n.

Русский

Для m ∈ ENat и n ∈ ℕ с условием AtLeastTwo, (m : Cardinal) = ofNat n ↔ m = OfNat.ofNat n.

LaTeX

$$∀ {m : ENat} {n : Nat} [n.AtLeastTwo], (m : Cardinal) = ofNat(n) ↔ m = OfNat.ofNat n$$

Lean4

@[simp]
theorem ofENat_eq_ofNat {m : ℕ∞} {n : ℕ} [n.AtLeastTwo] : (m : Cardinal) = ofNat(n) ↔ m = OfNat.ofNat n :=
  ofENat_eq_nat

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

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

Разделы

Аффилиация

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