Theorems · Definition · general topology

TendstoLocallyUniformlyOn

{α : Type u_1} →
  {β : Type u_2} →
    {ι : Type u_4} → [TopologicalSpace α] → [UniformSpace β] → (ι → α → β) → (α → β) → Filter ι → Set α → Prop

A sequence of functions Fₙ converges locally uniformly on a set s to a limiting function f with respect to a filter p if, for any entourage of the diagonal u, for any x ∈ s, one has p-eventually (f y, Fₙ y) ∈ u for all y in a neighborhood of x in s.

Defined in

Mathlib.Topology.UniformSpace.LocallyUniformConvergence

Cited by

84 results in Mathlib

Foundations

Depth 49 from the axioms · uses propext, Quot.sound

Assumes

TopologicalSpaceUniformSpace