Theorems · Theorem · general topology

UniformFun.uniformContinuous_toFun

∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace β], UniformContinuous ⇑UniformFun.toFun

The natural map UniformFun.toFun from α →ᵤ β to α → β is uniformly continuous. In other words, the uniform structure of uniform convergence is finer than that of pointwise convergence, aka the product uniform structure.

Defined in

Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Cited by

2 results in Mathlib

Foundations

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

Assumes

UniformSpace