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, тогда отображение пары образов является сюръективным между произведениями.
LaTeX
$$$ \\operatorname{SurjOn} f1 s1 t1 \\Rightarrow \\operatorname{SurjOn} f2 s2 t2 \\Rightarrow \\operatorname{SurjOn} (\\lambda x. (f1 x.1, f2 x.2)) (s1 \\times s2) (t1 \\times t2). $$$
Lean4
theorem prodMap (h₁ : SurjOn f₁ s₁ t₁) (h₂ : SurjOn f₂ s₂ t₂) :
SurjOn (fun x ↦ (f₁ x.1, f₂ x.2)) (s₁ ×ˢ s₂) (t₁ ×ˢ t₂) :=
by
rintro x hx
obtain ⟨a₁, ha₁, hx₁⟩ := h₁ hx.1
obtain ⟨a₂, ha₂, hx₂⟩ := h₂ hx.2
exact ⟨(a₁, a₂), ⟨ha₁, ha₂⟩, Prod.ext hx₁ hx₂⟩
