English
The natural uniform isomorphism between α →ᵤ[𝔖] (Π i, δ i) and (Π i, α →ᵤ[𝔖] δ i) is uniform inducing.
Русский
Естественная равномерная изоморфия между α →ᵤ[𝔖] (Π i, δ i) и (Π i, α →ᵤ[𝔖] δ i) является равномерно индуцирующей.
LaTeX
$$UniformOnFun.uniformEquivPiComm : (α →ᵤ[𝔖] ((i : ι) → δ i)) ≃ᵤ ((i : ι) → α →ᵤ[𝔖] δ i).$$
Lean4
/-- The natural bijection between `α → Π i, δ i` and `Π i, α → δ i`, upgraded to a uniform
isomorphism between `α →ᵤ[𝔖] (Π i, δ i)` and `Π i, α →ᵤ[𝔖] δ i`. -/
protected def uniformEquivPiComm : (α →ᵤ[𝔖] ((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
-- `UniformOnFun.iInf_eq` and `UniformOnFun.comap_eq`,
-- which leaves us to check that some square commutes.
-- We could also deduce this from `UniformFun.uniformEquivPiComm`, but it turns out
-- to be more annoying.
@Equiv.toUniformEquivOfIsUniformInducing (α →ᵤ[𝔖] ((i : ι) → δ i)) ((i : ι) → α →ᵤ[𝔖] δ i) _ _ (Equiv.piComm _) <|
by
constructor
change comap (Prod.map Function.swap Function.swap) _ = _
erw [← uniformity_comap]
congr
rw [Pi.uniformSpace, UniformSpace.ofCoreEq_toCore, Pi.uniformSpace, UniformSpace.ofCoreEq_toCore,
UniformSpace.comap_iInf, UniformOnFun.iInf_eq]
refine iInf_congr fun i => ?_
rw [← UniformSpace.comap_comap, UniformOnFun.comap_eq]
rfl
-- Like in the previous lemma, the diagram actually commutes by definition
