ofENat_eq_zero

Mathlib.SetTheory.Cardinal.ENat

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

English

For m ∈ ENat, (m : Cardinal) = 0 iff m = 0.

Русский

Для m ∈ ENat, (m : Cardinal) = 0 эквивалентно m = 0.

LaTeX

$$∀ {m : ENat}, (Cardinal.ofENat m) = 0 ↔ m = 0$$

Lean4

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

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

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

Разделы

Аффилиация

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