ofENat_pos

Mathlib.SetTheory.Cardinal.ENat

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

English

For any m ∈ ℕ∞, 0 < (m : Cardinal) if and only if 0 < m.

Русский

Для любого m ∈ ℕ∞ верно, что 0 < (m : Cardinal) ⇔ 0 < m.

LaTeX

$$0 < (m : \mathrm{Cardinal}) \iff 0 < m$$

Lean4

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

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

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

Разделы

Аффилиация

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