of_map — Mathlib

English

If map f s is noduplicate (Nodup), then s is noduplicate.

Русский

Если отображение f на множество s образует Nodup, то само множество s образует Nodup.

LaTeX

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

Lean4

theorem of_map (f : α → β) : Nodup (map f s) → Nodup s :=
  Quot.induction_on s fun _ => List.Nodup.of_map f

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