English
If h1 : BijOn f1 s1 t1 and h2 : BijOn f2 s2 t2, then the pair map is BijOn from s1 ×ˢ s2 to t1 ×ˢ t2.
Русский
Если h1 : BijOn f1 s1 t1 и h2 : BijOn f2 s2 t2, тогда отображение пары является биекцией между произведениями.
LaTeX
$$$ \\operatorname{BijOn} f1 s1 t1 \\Rightarrow \\operatorname{BijOn} f2 s2 t2 \\Rightarrow \\operatorname{BijOn} (fun x \\mapsto { fst := f1 x.1, snd := f2 x.2 }) (s1 \\timesˢ s2) (t1 \\timesˢ t2). $$$
Lean4
theorem prodMap (h₁ : BijOn f₁ s₁ t₁) (h₂ : BijOn f₂ s₂ t₂) : BijOn (fun x ↦ (f₁ x.1, f₂ x.2)) (s₁ ×ˢ s₂) (t₁ ×ˢ t₂) :=
⟨h₁.mapsTo.prodMap h₂.mapsTo, h₁.injOn.prodMap h₂.injOn, h₁.surjOn.prodMap h₂.surjOn⟩
