nodup_map_univ_iff_injective — Mathlib

English

For any [Fintype α], (Multiset.map f univ.val).Nodup is equivalent to Injective f.

Русский

Для любого [Fintype α] выражение (Multiset.map f univ.val).Nodup эквивалентно Injective f.

LaTeX

$$$$ (\mathrm{Multiset.map} f \mathrm{univ.val}).\mathrm{Nodup} \iff \mathrm{Function.Injective} f $$$$

Lean4

theorem nodup_map_univ_iff_injective [Fintype α] {f : α → β} : (Multiset.map f univ.val).Nodup ↔ Function.Injective f :=
  by rw [nodup_map_iff_injOn, coe_univ, Set.injective_iff_injOn_univ]

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