mk_fin

Mathlib.SetTheory.Cardinal.Order

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

English

The cardinality of Fin(n) is n, i.e., there are exactly n elements in Fin(n).

Русский

Кардинал Fin(n) равен n; в Fin(n) ровно n элементов.

LaTeX

$$$\#(\mathrm{Fin}(n)) = n$$$

Lean4

theorem mk_fin (n : ℕ) : #(Fin n) = n := by simp

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

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

Разделы

Аффилиация

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