English
If f: γ → β is uniformly continuous, then the postcomposition map g ↦ f ∘ g is uniformly continuous on the 𝔖-convergence spaces.
Русский
Если f: γ → β равномерно непрерывна, то отображение g ↦ f ∘ g равномерно непрерывно на пространствах 𝔖-сходимости.
LaTeX
$$UniformContinuous f → UniformContinuous (ofFun 𝔖 ∘ (f ∘ ·) ∘ toFun 𝔖).$$
Lean4
/-- Post-composition by a uniformly continuous function is uniformly continuous for the
uniform structures of `𝔖`-convergence.
More precisely, if `f : γ → β` is uniformly continuous, then
`(fun g ↦ f ∘ g) : (α →ᵤ[𝔖] γ) → (α →ᵤ[𝔖] β)` is uniformly continuous. -/
protected theorem postcomp_uniformContinuous [UniformSpace γ] {f : γ → β} (hf : UniformContinuous f) :
UniformContinuous (ofFun 𝔖 ∘ (f ∘ ·) ∘ toFun 𝔖) := by
-- This is a direct consequence of `UniformOnFun.comap_eq`
rw [uniformContinuous_iff]
exact (UniformOnFun.mono (uniformContinuous_iff.mp hf) subset_rfl).trans_eq UniformOnFun.comap_eq
