English
A function f is surjective on s onto t if and only if there exists a subset s' of s such that f maps s' bijectively onto t.
Русский
Функция f сюръективна на s на t тогда и только тогда, когда существует подмножество s' ⊆ s such that f ограничено на s' даёт биекция на t.
LaTeX
$$$SurjOn\ f\ s\ t \\Leftrightarrow \\exists s' \\subseteq s, BijOn\ f\ s'\\ t$$$
Lean4
theorem surjOn_iff_exists_bijOn_subset : SurjOn f s t ↔ ∃ s' ⊆ s, BijOn f s' t :=
by
constructor
· rcases eq_empty_or_nonempty t with (rfl | ht)
· exact fun _ => ⟨∅, empty_subset _, bijOn_empty f⟩
· intro h
haveI : Nonempty α := ⟨Classical.choose (h.comap_nonempty ht)⟩
exact ⟨_, h.mapsTo_invFunOn.image_subset, h.bijOn_subset⟩
· rintro ⟨s', hs', hfs'⟩
exact hfs'.surjOn.mono hs' (Subset.refl _)
