toFinset_card_of_nodup

Mathlib.Data.Finset.Card

URI: https://scilib.ai/kg/mathlib#Multiset.toFinset_card_of_nodup

English

If m is nodup, then the finset obtained by dedup has the same cardinality as m.

Русский

Если m имеет без повторов, то m.toFinset имеет ту же кардинальность, что и m.

LaTeX

$$Nodup(m) \Rightarrow #m.toFinset = \operatorname{card} m$$

Lean4

theorem toFinset_card_of_nodup {m : Multiset α} (h : m.Nodup) : #m.toFinset = Multiset.card m :=
  congr_arg card <| Multiset.dedup_eq_self.mpr h

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

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

Разделы

Аффилиация

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