toFinset_card_eq_card_iff_nodup

Mathlib.Data.Finset.Card

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

English

The same equivalence as above for the toFinset pairing with nodup.

Русский

Аналогично для toFinset и Nodup.

LaTeX

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

Lean4

theorem toFinset_card_eq_card_iff_nodup {m : Multiset α} : #m.toFinset = card m ↔ m.Nodup :=
  dedup_card_eq_card_iff_nodup

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

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

Разделы

Аффилиация

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