English
If h1 : LeftInvOn g1 f1 s1 and h2 : LeftInvOn g2 f2 s2, then the pair-map x ↦ (g1 x.1, g2 x.2) is LeftInvOn with the pair f-map.
Русский
Если h1: LeftInvOn g1 f1 s1 и h2: LeftInvOn g2 f2 s2, то отображение x ↦ (g1 x.1, g2 x.2) сохраняет левый инверс на произведении.
LaTeX
$$$ \\operatorname{LeftInvOn} g1 f1 s1 \\Rightarrow \\operatorname{LeftInvOn} g2 f2 s2 \\Rightarrow \\operatorname{LeftInvOn} (\\lambda x. (g1 x.1, g2 x.2)) (\\lambda x. (f1 x.1, f2 x.2)) (s1 \\times s2). $$$
Lean4
protected theorem extendDomain (h : RightInvOn g₁ g₂ t) :
RightInvOn (g₁.extendDomain f) (g₂.extendDomain f) ((↑) ∘ f '' t) := by rintro _ ⟨a, ha, rfl⟩;
simp_rw [Function.comp_apply, extendDomain_apply_image, h ha]
