mk_toNat_eq_card

Mathlib.SetTheory.Cardinal.ToNat

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

English

For a finite type α, the toNat of its cardinal is equal to the finite card of α: toNat(#α) = card α.

Русский

Для конечного множества α: toNat(#α) = card α.

LaTeX

$$$\text{If } \alpha \text{ is finite},\ toNat(#\alpha) = \operatorname{Fintype.card}(\alpha).$$$

Lean4

theorem mk_toNat_eq_card [Fintype α] : toNat #α = Fintype.card α := by simp

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

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

Разделы

Аффилиация

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