English
If h1 : LeftInvOn g1 f1 s1 and h2 : LeftInvOn g2 f2 s2, then the pair map is LeftInvOn for the pair of functions on the product sets.
Русский
Если h1: LeftInvOn g1 f1 s1 и h2: LeftInvOn g2 f2 s2, тогда отображение пары сохраняет левый инверс на произведении.
LaTeX
$$$ \\operatorname{LeftInvOn} g1 f1 s1 \\Rightarrow \\operatorname{LeftInvOn} g2 f2 s2 \\Rightarrow \\operatorname{LeftInvOn} (fun x. (g1 x.1, g2 x.2)) (fun x. (f1 x.1, f2 x.2)) (s1 \\timesˢ s2). $$$
Lean4
theorem prodMap (h₁ : LeftInvOn g₁ f₁ s₁) (h₂ : LeftInvOn g₂ f₂ s₂) :
LeftInvOn (fun x ↦ (g₁ x.1, g₂ x.2)) (fun x ↦ (f₁ x.1, f₂ x.2)) (s₁ ×ˢ s₂) := fun _x hx ↦
Prod.ext (h₁ hx.1) (h₂ hx.2)
