Theorems · Theorem · general topology

continuous_from_uCompactlyGeneratedSpace

∀ {X : Type w} {Y : Type x} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] [UCompactlyGeneratedSpace X]
  (f : X → Y), (∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous (f ∘ ⇑g)) → Continuous f

If X is compactly generated, to prove that f : X → Y is continuous it is enough to show that for every compact Hausdorff space K and every continuous map g : K → X, f ∘ g is continuous.

Defined in

Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceUCompactlyGeneratedSpace