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