nat_eq_ofENat

Mathlib.SetTheory.Cardinal.ENat

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

English

For m ∈ Nat and n ∈ ENat, (m : Cardinal) = n ↔ m = n.

Русский

Для m ∈ Nat и n ∈ ENat, (m : Cardinal) = n ↔ m = n.

LaTeX

$$∀ {m : Nat} {n : ENat}, (m : Cardinal) = n ↔ m = n$$

Lean4

@[simp]
theorem nat_eq_ofENat {m : ℕ} {n : ℕ∞} : (m : Cardinal) = n ↔ m = n := by norm_cast

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

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

Разделы

Аффилиация

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