Theorems · Theorem · general topology

ContinuousMap.tendsto_iff_tendstoUniformly

∀ {α : Type u₁} {β : Type u₂} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {f : C(α, β)} {ι : Type u₃}
  {p : Filter ι} {F : ι → C(α, β)} [CompactSpace α],
  Filter.Tendsto F p (nhds f) ↔ TendstoUniformly (fun i a => (F i) a) (⇑f) p

Convergence in the compact-open topology is the same as uniform convergence for sequences of continuous functions on a compact space.

Defined in

Mathlib.Topology.UniformSpace.CompactConvergence

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceUniformSpaceCompactSpace