Theorems · Theorem · general topology

UniformOnFun.tendsto_iff_tendstoUniformlyOn

∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} {p : Filter ι} [inst : UniformSpace β] {𝔖 : Set (Set α)}
  {F : ι → UniformOnFun α β 𝔖} {f : UniformOnFun α β 𝔖},
  Filter.Tendsto F p (nhds f) ↔ ∀ s ∈ 𝔖, TendstoUniformlyOn (⇑(UniformOnFun.toFun 𝔖) ∘ F) ((UniformOnFun.toFun 𝔖) f) p s

Convergence in the topology of 𝔖-convergence means uniform convergence on S (in the sense of TendstoUniformlyOn) for all S ∈ 𝔖.

Defined in

Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Cited by

5 results in Mathlib

Foundations

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

Assumes

UniformSpace