English
If f maps s to t, is surjective on s to t, and |s| ≤ |t|, then f is injective on s.
Русский
Если f отображает s в t, сюръективно отображает s на t, и |s| ≤ |t|, то f инъективно на s.
LaTeX
$$MapsTo f s t ∧ SurjOn f s t ∧ |s| ≤ |t| ⇒ InjOn f s$$
Lean4
/-- Given a surjective map `f` from a finite set `s` to another finite set `t`, if `s` is no larger
than `t`, then `f` is injective when restricted to `s`.
See `Finset.inj_on_of_surj_on_of_card_le` for the version where `f` is a dependent function.
-/
theorem injOn_of_surjOn_of_card_le (f : α → β) (hf : Set.MapsTo f s t) (hsurj : Set.SurjOn f s t) (hst : #s ≤ #t) :
Set.InjOn f s := by
classical
have : s.image f = t := Finset.coe_injective <| by simp [hsurj.image_eq_of_mapsTo hf]
have : #(s.image f) = #t := by rw [this]
have : #(s.image f) ≤ #s := card_image_le
rw [← card_image_iff]
cutsat
