mk_toNat_of_infinite

Mathlib.SetTheory.Cardinal.ToNat

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

English

If α is infinite, then the natural part of its cardinal is 0: toNat(#α) = 0.

Русский

Если множество бесконечно, то его кардинал имеет toNat равное 0: toNat(#α) = 0.

LaTeX

$$$\text{If } \alpha \text{ is infinite, then } toNat(#\alpha) = 0.$$$

Lean4

@[simp]
theorem mk_toNat_of_infinite [h : Infinite α] : toNat #α = 0 := by simp

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

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

Разделы

Аффилиация

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