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