Theorems · Definition · general topology

TendstoUniformlyOn

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

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

Defined in

Mathlib.Topology.UniformSpace.UniformConvergence

Cited by

129 results in Mathlib

Foundations

Depth 6 from the axioms, rests on 16 definitions · uses no axioms

Assumes

UniformSpace