dedup_card_eq_card_iff_nodup — Mathlib

English

The deduplicated card equals the original card iff the multiset has no repeats.

Русский

Кардинал m.dedup равен кардиналу m тогда и только тогда, когда у m нет повторов.

LaTeX

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

Lean4

theorem dedup_card_eq_card_iff_nodup {m : Multiset α} : card m.dedup = card m ↔ m.Nodup :=
  .trans ⟨fun h ↦ eq_of_le_of_card_le (dedup_le m) h.ge, congr_arg _⟩ dedup_eq_self

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