Theorems · Theorem · general topology

UniformFun.precomp_uniformContinuous

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : UniformSpace β] {f : γ → α},
  UniformContinuous fun g => UniformFun.ofFun (UniformFun.toFun g ∘ f)

Pre-composition by any function is uniformly continuous for the uniform structures of uniform convergence. More precisely, for any f : γ → α, the function (· ∘ f) : (α →ᵤ β) → (γ →ᵤ β) is uniformly continuous.

Defined in

Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Cited by

2 results in Mathlib

Foundations

Depth 70 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

UniformSpace