Theorems · Theorem · general topology

EquicontinuousAt.tendsto_of_mem_closure

∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] {l : Filter ι}
  {F : ι → X → α} {f : X → α} {s : Set X} {x : X} {z : α},
  EquicontinuousAt F x →
    Filter.Tendsto f (nhdsWithin x s) (nhds z) →
      (∀ y ∈ s, Filter.Tendsto (fun x => F x y) l (nhds (f y))) →
        x ∈ closure s → Filter.Tendsto (fun x_1 => F x_1 x) l (nhds z)

If F : ι → X → α is a family of functions equicontinuous at x, it tends to f y along a filter l for any y ∈ s, the limit function f tends to z along 𝓝[s] x, and x ∈ closure s, then (F · x) tends to z along l. In some sense, this is a converse of EquicontinuousAt.closure.

Defined in

Mathlib.Topology.UniformSpace.Equicontinuity

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceUniformSpace