English
If h1 : InjOn f1 s1 and h2 : InjOn f2 s2, then the function x ↦ { fst := f1 x.fst, snd := f2 x.snd } is InjOn on s1 × s2.
Русский
Если h1 : InjOn f1 s1 и h2 : InjOn f2 s2, тогда отображение пары инъективно на произведении.
LaTeX
$$$ \\operatorname{InjOn} f1 s1 \\Rightarrow \\operatorname{InjOn} f2 s2 \\Rightarrow \\operatorname{InjOn} (fun x => \\{ fst := f1 x.fst, snd := f2 x.snd \\}) (\\operatorname{instSProd.sprod} s1 s2). $$$
Lean4
theorem prodMap (h₁ : s₁.InjOn f₁) (h₂ : s₂.InjOn f₂) : (s₁ ×ˢ s₂).InjOn fun x ↦ (f₁ x.1, f₂ x.2) := fun x hx y hy ↦ by
simp_rw [Prod.ext_iff]; exact And.imp (h₁ hx.1 hy.1) (h₂ hx.2 hy.2)
