length_sort

Mathlib.Data.Finset.Sort

URI: https://scilib.ai/kg/mathlib#Finset.length_sort

English

The length of the sorted list of a Finset s equals the cardinality of s.

Русский

Длина отсортированного списка множества s равна мощности множества s.

LaTeX

$$$ (\\operatorname{sort}_r(s)).length = s.card $$$

Lean4

@[simp]
theorem length_sort {s : Finset α} : (sort r s).length = s.card :=
  Multiset.length_sort _

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

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

Разделы

Аффилиация

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