nodup_map_iff_injOn — Mathlib

English

For any f : α → β and Finset s, the mapped multiset (Multiset.map f s.val) is nodup iff f is injective on s.

Русский

Для любого отображения f : α → β и Finset s, отображение Multiset.map f s.val не содержит повторов тогда и только если f инъективно на s.

LaTeX

$$$$(\mathrm{Multiset.map } f\, s.\mathrm{val}).\mathrm{Nodup} \iff \mathrm{Set.InjOn} f\ s$$$$

Lean4

theorem nodup_map_iff_injOn {f : α → β} {s : Finset α} : (Multiset.map f s.val).Nodup ↔ Set.InjOn f s := by
  simp [Multiset.nodup_map_iff_inj_on s.nodup, Set.InjOn]

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