Theorems · Theorem · general topology

Filter.Tendsto.continuousWithinAt_of_equicontinuousWithinAt

∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] {l : Filter ι} [l.NeBot]
  {F : ι → X → α} {f : X → α} {S : Set X} {x₀ : X},
  (∀ x ∈ S, Filter.Tendsto (fun x_1 => F x_1 x) l (nhds (f x))) →
    Filter.Tendsto (fun x => F x x₀) l (nhds (f x₀)) → EquicontinuousWithinAt F S x₀ → ContinuousWithinAt f S x₀

If 𝓕 : ι → X → α tends to f : X → α pointwise on `S ∪ {x₀} : Set X` along some nontrivial filter, and if the family 𝓕 is equicontinuous at x₀ : X within S, then the limit is continuous at x₀ within S.

Defined in

Mathlib.Topology.UniformSpace.Equicontinuity

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceUniformSpaceFilter.NeBot