Theorems · Theorem · general topology

UniformOnFun.uniformContinuous_eval_of_mem

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

If x : α is in some S ∈ 𝔖, then evaluation at x is uniformly continuous on α →ᵤ[𝔖] β.

Defined in

Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Cited by

4 results in Mathlib

Foundations

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

Assumes

UniformSpace