Lean4
/-- The natural bijection between `α → Π i, δ i` and `Π i, α → δ i`, upgraded to a uniform
isomorphism between `α →ᵤ (Π i, δ i)` and `Π i, α →ᵤ δ i`. -/
protected def uniformEquivPiComm : UniformEquiv (α →ᵤ ∀ i, δ i) (∀ i, α →ᵤ δ i) :=
-- Denote `φ` this bijection. We want to show that
-- `comap φ (Π i, 𝒰(α, δ i, uδ i)) = 𝒰(α, (Π i, δ i), (Π i, uδ i))`.
-- But `Π i, uδ i` is defined as `⨅ i, comap (eval i) (uδ i)`, so we just have to apply
-- `UniformFun.iInf_eq` and `UniformFun.comap_eq`, which leaves us to check
-- that some square commutes.
@Equiv.toUniformEquivOfIsUniformInducing _ _ 𝒰(α, ∀ i, δ i, Pi.uniformSpace δ)
(@Pi.uniformSpace ι (fun i => α → δ i) fun i => 𝒰(α, δ i, _)) (Equiv.piComm _) <|
by
refine @IsUniformInducing.mk ?_ ?_ ?_ ?_ ?_ ?_
change comap (Prod.map Function.swap Function.swap) _ = _
rw [← uniformity_comap]
congr
unfold Pi.uniformSpace
rw [UniformSpace.ofCoreEq_toCore, UniformSpace.ofCoreEq_toCore, UniformSpace.comap_iInf, UniformFun.iInf_eq]
refine iInf_congr fun i => ?_
rw [← UniformSpace.comap_comap, UniformFun.comap_eq]
rfl
-- Like in the previous lemma, the diagram actually commutes by definition
