English
If h1 : SurjOn f1 s1 t1 and h2 : SurjOn f2 s2 t2, then the map x ↦ (f1 x.1, f2 x.2) is SurjOn from s1 × s2 to t1 × t2.
Русский
Если h1 : SurjOn f1 s1 t1 и h2 : SurjOn f2 s2 t2, тогда отображение x ↦ (f1 x.1, f2 x.2) является сюръективным между произведениями.
LaTeX
$$$ \\operatorname{SurjOn} f1 s1 t1 \\Rightarrow \\operatorname{SurjOn} f2 s2 t2 \\Rightarrow \\operatorname{SurjOn} (fun x \\mapsto (f1 x.1, f2 x.2)) (s1 \\times\\! s2) (t1 \\times\\! t2). $$$
Lean4
protected theorem extendDomain (h : BijOn g s t) : BijOn (g.extendDomain f) ((↑) ∘ f '' s) ((↑) ∘ f '' t) :=
⟨h.mapsTo.extendDomain, (g.extendDomain f).injective.injOn, h.surjOn.extendDomain⟩
