injOn_of_encard_image_eq — Mathlib

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

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