length_sortedUniv

Mathlib.Logic.Equiv.Finset

URI: https://scilib.ai/kg/mathlib#Encodable.length_sortedUniv

English

The length of sortedUniv α equals the cardinality of α.

Русский

Длина sortedUniv α равна мощности α.

LaTeX

$$$ |\\mathrm{sortedUniv}(\\alpha)| = \\operatorname{Fintype.card}(\\alpha) $$$

Lean4

@[simp]
theorem length_sortedUniv (α) [Fintype α] [Encodable α] : (sortedUniv α).length = Fintype.card α :=
  Finset.length_sort _

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

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

Разделы

Аффилиация

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