Theorems · Theorem · general topology

uCompactlyGeneratedSpace_of_continuous_maps

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

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

Defined in

Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Cited by

3 results in Mathlib

Foundations

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

Assumes

TopologicalSpace