ofNat_eq_ofENat

Mathlib.SetTheory.Cardinal.ENat

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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