English
For any finite set S and function f, the image cardinality |f[S]| equals |S| if and only if f is injective on S.
Русский
Для конечного множества S и функции f справедливо, что |f[S]| = |S| тогда и только тогда, когда f инъективна на S.
LaTeX
$$$|f[S]| = |S| \\iff \\forall x,y \\in S,\\; f(x) = f(y) \\Rightarrow x = y$$$
Lean4
theorem card_image_iff [DecidableEq β] : #(s.image f) = #s ↔ Set.InjOn f s :=
⟨injOn_of_card_image_eq, card_image_of_injOn⟩