Theorems · Theorem · general topology

Set.EquicontinuousAt.closure

∀ {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] {A : Set (X → α)} {x₀ : X},
  A.EquicontinuousAt x₀ → (closure A).EquicontinuousAt x₀

If a set of functions is equicontinuous at some x₀, its closure for the product topology is also equicontinuous at x₀.

Defined in

Mathlib.Topology.UniformSpace.Equicontinuity

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceUniformSpace