English
Convergence in the 𝔖-convergence topology is equivalent to uniform convergence on each S ∈ 𝔖.
Русский
Сходимость в топологии 𝔖-конвергенции эквивалентна равномерной сходимости на каждом S ∈ 𝔖.
LaTeX
$$Tendsto F p (nhds f) ⇔ ∀ s ∈ 𝔖, TendstoUniformlyOn (toFun 𝔖 ∘ F) (toFun 𝔖 f) p s.$$
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
-- `UniformOnFun.inf_eq` and `UniformOnFun.comap_eq`,
-- which leaves us to check that some square commutes.
-- We could also deduce this from `UniformFun.uniformEquivProdArrow`,
-- but it turns out to be more annoying.
((UniformOnFun.ofFun 𝔖).symm.trans <|
(Equiv.arrowProdEquivProdArrow _ _ _).trans <|
(UniformOnFun.ofFun 𝔖).prodCongr (UniformOnFun.ofFun 𝔖)).toUniformEquivOfIsUniformInducing <|
by
constructor
rw [uniformity_prod, comap_inf, comap_comap, comap_comap]
have H := @UniformOnFun.inf_eq α (β × γ) 𝔖 (UniformSpace.comap Prod.fst ‹_›) (UniformSpace.comap Prod.snd ‹_›)
apply_fun (fun u ↦ @uniformity (α →ᵤ[𝔖] β × γ) u) at H
convert H.symm using 1
rw [UniformOnFun.comap_eq, UniformOnFun.comap_eq]
erw [inf_uniformity]
rw [uniformity_comap, uniformity_comap]
rfl
-- the relevant diagram commutes by definition
