Theorems · Theorem · general topology

UniformOnFun.uniformContinuous_restrict

∀ (α : Type u_1) (β : Type u_2) {s : Set α} [inst : UniformSpace β] (𝔖 : Set (Set α)),
  s ∈ 𝔖 → UniformContinuous (⇑UniformFun.ofFun ∘ s.domRestrict ∘ ⇑(UniformOnFun.toFun 𝔖))

If S ∈ 𝔖, then the restriction to S is a uniformly continuous map from α →ᵤ[𝔖] β to ↥S →ᵤ β.

Defined in

Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Cited by

1 results in Mathlib

Foundations

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

Assumes

UniformSpace