English
If hs is finite and (f '' s).encard = s.encard, then f is injOn s.
Русский
Пусть hs конечно и (f''s).encard = s.encard, тогда f injOn s.
LaTeX
$$If hs and (f''s).encard = s.encard then InjOn f s$$
Lean4
theorem injOn_of_encard_image_eq (hs : s.Finite) (h : (f '' s).encard = s.encard) : InjOn f s :=
by
obtain (h' | hne) := isEmpty_or_nonempty α
· simp
rw [← (f.invFunOn_injOn_image s).encard_image] at h
rw [injOn_iff_invFunOn_image_image_eq_self]
exact hs.eq_of_subset_of_encard_le' (f.invFunOn_image_image_subset s) h.symm.le