English
There is an equivalence: Nodup (map f s) iff Nodup s, under a suitable inj_on condition: the dependence of f on membership in s is irrelevant if Nodup holds.
Русский
Существует эквиваленция: Nodup (map f s) ⇔ Nodup s при условии подходящей inj_on-условности: зависимость f от принадлежности элементов не влияет при Nodup.
LaTeX
$$$\\forall {s : \\mathrm{Multiset}\\\\ \\alpha}, {f : \\alpha \\\\to \\beta}, (\\\\forall x \\\\in s \\\\forall y \\\\in s, f x = f y \\\\Rightarrow x = y) \\\\Rightarrow \\\\mathrm{Nodup}(\\\\mathrm{map}\\\\ f\\\\ s) \\\\Leftrightarrow \\\\mathrm{Nodup} s.$$$
Lean4
theorem nodup_map_iff_of_inj_on {f : α → β} (d : ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y) : Nodup (map f s) ↔ Nodup s :=
⟨Nodup.of_map _, fun h => h.map_on d⟩
