English
A surjection on a set can be represented via a map to a subtype of the codomain with a surjective restriction, preserving f on s.
Русский
Сюръон на s можно представить через отображение в подмножество значения целевого множества с сюръективным ограничением, сохраняя значения f на s.
LaTeX
$$$\\text{SurjOn } f s t \\iff \\exists t' \\subseteq \\beta, (g: s \\to t')\\text{ surjective}, \\forall x\\in s, f(x)=g(x).$$$
Lean4
theorem surjOn_iff_exists_map_subtype :
SurjOn f s t ↔ ∃ (t' : Set β) (g : s → t'), t ⊆ t' ∧ Surjective g ∧ ∀ x : s, f x = g x :=
⟨fun h => ⟨_, (mapsTo_image f s).restrict f s _, h, surjective_mapsTo_image_restrict _ _, fun _ => rfl⟩,
fun ⟨t', g, htt', hg, hfg⟩ y hy =>
let ⟨x, hx⟩ := hg ⟨y, htt' hy⟩
⟨x, x.2, by rw [hfg, hx, Subtype.coe_mk]⟩⟩
