English
Product of two uniform isomorphisms is a uniform isomorphism between products.
Русский
Произведение двух униформных изоморфизмов является униформным изоморфизмом между произведениями.
LaTeX
$$$\\forall {\\alpha \\beta \\gamma \\delta} [UniformSpace \\alpha] [UniformSpace \\beta] [UniformSpace \\gamma] [UniformSpace \\delta],\\; (\\alpha \\simeq_u \\beta) \\Rightarrow (\\gamma \\simeq_u \\delta) \\Rightarrow (\\alpha \\times \\gamma) \\simeq_u (\\beta \\times \\delta)$$$
Lean4
/-- Product of two uniform isomorphisms. -/
def prodCongr (h₁ : α ≃ᵤ β) (h₂ : γ ≃ᵤ δ) : α × γ ≃ᵤ β × δ
where
uniformContinuous_toFun :=
(h₁.uniformContinuous.comp uniformContinuous_fst).prodMk (h₂.uniformContinuous.comp uniformContinuous_snd)
uniformContinuous_invFun :=
(h₁.symm.uniformContinuous.comp uniformContinuous_fst).prodMk (h₂.symm.uniformContinuous.comp uniformContinuous_snd)
toEquiv := h₁.toEquiv.prodCongr h₂.toEquiv
