Theorems · Theorem · general topology

ContinuousMap.tendsto_compactOpen_iff_forall

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

Defined in

Mathlib.Topology.CompactOpen

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace