map — Mathlib

English

If f is injective, then Nodup s implies Nodup (map f s).

Русский

Если f инъективна, то узкая повторяемость сохраняется: Nodup s => Nodup (map f s).

LaTeX

$$$\\forall {f : \\alpha \\to \\beta},\\\\(Injective f) \\\\Rightarrow \\\\mathrm{Nodup} s \\\\Rightarrow \\\\mathrm{Nodup}(\\\\mathrm{map}\\\\ f\\\\ s).$$$

Lean4

theorem map {f : α → β} {s : Multiset α} (hf : Injective f) : Nodup s → Nodup (map f s) :=
  Nodup.map_on fun _ _ _ _ h => hf h

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