dedup_map_of_injective — Mathlib

English

If f is injective, then dedup commutes with map: dedup(map f s) = map f (dedup s).

Русский

Если f инъективна, то удаление повторов commute с отображением: dedup(map f s) = map f (dedup s).

LaTeX

$$$$Injective(f) \Rightarrow (map\ f\ s).dedup = map\ f\ (s.dedup)$$$$

Lean4

theorem dedup_map_of_injective [DecidableEq β] {f : α → β} (hf : Function.Injective f) (s : Multiset α) :
    (s.map f).dedup = s.dedup.map f :=
  Quot.induction_on s fun l => by simp [List.dedup_map_of_injective hf l]

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