Theorems · Theorem · general topology

tendstoUniformlyOnFilter_iff_tendsto

∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι}
  {p' : Filter α},
  TendstoUniformlyOnFilter F f p p' ↔ Filter.Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ p') (uniformity β)

A sequence of functions Fₙ converges uniformly on a filter p' to a limiting function f w.r.t. filter p iff the function (n, x) ↦ (f x, Fₙ x) converges along p ×ˢ p' to the uniformity. In other words: one knows nothing about the behavior of x in this limit besides it being in p'.

Defined in

Mathlib.Topology.UniformSpace.UniformConvergence

Cited by

4 results in Mathlib

Foundations

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

Assumes

UniformSpace