English
The natural bijection between α → β × γ and (α → β) × (α → γ) extends to a uniform isomorphism between α →ᵤ β × γ and (α →ᵤ β) × (α →ᵤ γ).
Русский
Естественная биекция между α → β × γ и (α → β) × (α → γ) распространяется на равномерный изоморфизм между α →ᵤ β × γ и (α →ᵤ β) × (α →ᵤ γ).
LaTeX
$$$$ (α →^{u} β × γ) \simeq_{u} (α →^{u} β) \times (α →^{u} γ). $$$$
Lean4
/-- The natural bijection between `α → β × γ` and `(α → β) × (α → γ)`, upgraded to a uniform
isomorphism between `α →ᵤ β × γ` and `(α →ᵤ β) × (α →ᵤ γ)`. -/
protected def uniformEquivProdArrow [UniformSpace γ] : (α →ᵤ β × γ) ≃ᵤ (α →ᵤ β) × (α →ᵤ γ) :=
-- Denote `φ` this bijection. We want to show that
-- `comap φ (𝒰(α, β, uβ) × 𝒰(α, γ, uγ)) = 𝒰(α, β × γ, uβ × uγ)`.
-- But `uβ × uγ` is defined as `comap fst uβ ⊓ comap snd uγ`, so we just have to apply
-- `UniformFun.inf_eq` and `UniformFun.comap_eq`, which leaves us to check
-- that some square commutes.
Equiv.toUniformEquivOfIsUniformInducing (Equiv.arrowProdEquivProdArrow _ _ _) <|
by
constructor
change comap (Prod.map (Equiv.arrowProdEquivProdArrow _ _ _) (Equiv.arrowProdEquivProdArrow _ _ _)) _ = _
simp_rw [UniformFun]
rw [← uniformity_comap]
congr
unfold instUniformSpaceProd
rw [UniformSpace.comap_inf, ← UniformSpace.comap_comap, ← UniformSpace.comap_comap]
have := (@UniformFun.inf_eq α (β × γ) (UniformSpace.comap Prod.fst ‹_›) (UniformSpace.comap Prod.snd ‹_›)).symm
rwa [UniformFun.comap_eq, UniformFun.comap_eq] at this
