English
If f maps s into t, is injective on s, and |t| ≤ |s|, then f is surjective onto t from s.
Русский
Если f отображает s в t, инъективно на s, и |t| ≤ |s|, то f обладает сюръективностью на t.
LaTeX
$$MapsTo f s t ∧ InjOn f s ∧ |t| ≤ |s| ⇒ SurjOn f s t$$
Lean4
/-- Given an injective map `f` from a finite set `s` to another finite set `t`, if `t` is no larger
than `s`, then `f` is surjective to `t` when restricted to `s`.
See `Finset.surj_on_of_inj_on_of_card_le` for the version where `f` is a dependent function.
-/
theorem surjOn_of_injOn_of_card_le (f : α → β) (hf : Set.MapsTo f s t) (hinj : Set.InjOn f s) (hst : #t ≤ #s) :
Set.SurjOn f s t := by
classical
suffices s.image f = t by simp [← this, Set.SurjOn]
have : s.image f ⊆ t := by aesop (add simp Finset.subset_iff)
exact eq_of_subset_of_card_le this (hst.trans_eq (card_image_of_injOn hinj).symm)
