English
Let p be a predicate on α and f assign to each a ∈ s a value in β depending on a and a proof that p a holds. If the mapping a ↦ f a ha is injective with respect to a and its witness ha, then applying pmap to a Nodup multiset s yields a Nodup multiset, i.e., no duplicates appear after mapping.
Русский
Пусть p — признак на α, и для каждого элемента a множества s дано значение в β посредством f a ha, зависящее от a и доказательства p a. Если отображение a ↦ f a ha по элементам и их доказательствам является инъективным, то применение pmap к Nodup-множесту s сохраняет уникальность элементов (получаем Nodup).
LaTeX
$$$\\forall p:\\alpha\\to\\mathrm{Prop},\\;\\forall f:\\forall a,\\;p\\,a\\to\\beta,\\;\\forall s:\\mathrm{Multiset}\\ \\alpha,\\;\\forall H,\\;\\big(\\forall a\\ ha\\ b\\ hb,\\; f\\ a\\ ha = f\\ b\\ hb \\Rightarrow a = b\\big) \\Rightarrow \\operatorname{Nodup}(s) \\Rightarrow \\operatorname{Nodup}(\\mathrm{pmap}\\ f\\ s\\ H).$$$
Lean4
theorem pmap {p : α → Prop} {f : ∀ a, p a → β} {s : Multiset α} {H} (hf : ∀ a ha b hb, f a ha = f b hb → a = b) :
Nodup s → Nodup (pmap f s H) :=
Quot.induction_on s (fun _ _ => List.Nodup.pmap hf) H
