English
Precomposition by any function is uniformly continuous on the uniform convergence structures: for any f : γ → α, the map g ↦ g ∘ f is uniformly continuous from α →ᵤ β to γ →ᵤ β.
Русский
Пред-композиция любой функции равномерно непрерывна на структурах равномерной конвергенции: g ↦ g ∘ f.
LaTeX
$$$$ \text{For any } f: \gamma \to \alpha,\; (\lambda g: α \to^{u} β. g \circ f) : (α \to^{u} β) \to (\gamma \to^{u} β) \text{ is uniformly continuous}. $$$$
Lean4
/-- Post-composition by a uniformly continuous function is uniformly continuous on `α →ᵤ β`.
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 `UniformFun.comap_eq`
refine uniformContinuous_iff.mpr ?_
calc
𝒰(α, γ, _) ≤ 𝒰(α, γ, ‹UniformSpace β›.comap f) := UniformFun.mono (uniformContinuous_iff.mp hf)
_ = 𝒰(α, β, _).comap (f ∘ ·) := by exact UniformFun.comap_eq
