Theorems · Theorem · general topology

UniformOnFun.uniformContinuous_toFun

∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace β] {𝔖 : Set (Set α)},
  ⋃₀ 𝔖 = Set.univ → UniformContinuous ⇑(UniformOnFun.toFun 𝔖)

If 𝔖 covers α, the natural map UniformOnFun.toFun from α →ᵤ[𝔖] β to α → β is uniformly continuous. In other words, if 𝔖 covers α, then the uniform structure of 𝔖-convergence is finer than that of pointwise convergence.

Defined in

Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Cited by

2 results in Mathlib

Foundations

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

Assumes

UniformSpace