English
Let S be finite and f a function. If the cardinality of the image of S under f equals the cardinality of S, then f is injective on S.
Русский
Пусть S конечное множество и f: S → …. Если кардинал образа S под действием f равен кардиналу S, то f инъективна на S.
LaTeX
$$$|f[S]| = |S| \\Rightarrow \\forall x,y \\in S,\\; f(x) = f(y) \\Rightarrow x = y$$$
Lean4
theorem injOn_of_card_image_eq [DecidableEq β] (H : #(s.image f) = #s) : Set.InjOn f s :=
by
rw [card_def, card_def, image, toFinset] at H
dsimp only at H
have : (s.1.map f).dedup = s.1.map f :=
by
refine Multiset.eq_of_le_of_card_le (Multiset.dedup_le _) ?_
simp only [H, Multiset.card_map, le_rfl]
rw [Multiset.dedup_eq_self] at this
exact inj_on_of_nodup_map this
