English
If s is infinite and the image f''s is finite, then f is not injective on s.
Русский
Если s бесконечно, а образ f(s) конечен, то f не инъективна на s.
LaTeX
$$$ s.Infinite \land (f''s).Finite \Rightarrow ¬\operatorname{InjOn}(f,s) $$$
Lean4
theorem not_injOn_infinite_finite_image {f : α → β} {s : Set α} (h_inf : s.Infinite) (h_fin : (f '' s).Finite) :
¬InjOn f s := by
have : Finite (f '' s) := finite_coe_iff.mpr h_fin
have : Infinite s := infinite_coe_iff.mpr h_inf
have h := not_injective_infinite_finite ((f '' s).codRestrict (s.restrict f) fun x => ⟨x, x.property, rfl⟩)
contrapose! h
rwa [injective_codRestrict, ← injOn_iff_injective]