Theorems · Theorem · general topology

ContinuousMap.exists_tendsto_compactOpen_iff_forall

∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [WeaklyLocallyCompactSpace X]
  [T2Space Y] {ι : Type u_6} {l : Filter ι} [l.NeBot] (F : ι → C(X, Y)),
  (∃ f, Filter.Tendsto F l (nhds f)) ↔
    ∀ (s : Set X), IsCompact s → ∃ f, Filter.Tendsto (fun i => ContinuousMap.restrict s (F i)) l (nhds f)

A family F of functions in C(X, Y) converges in the compact-open topology, if and only if it converges in the compact-open topology on each compact subset of X.

Defined in

Mathlib.Topology.CompactOpen

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceWeaklyLocallyCompactSpaceT2SpaceFilter.NeBot