not_injOn_infinite_finite_image — Mathlib

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]

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