Theorems · Theorem · general topology

compactlyGeneratedSpace_of_continuous_maps

∀ {X : Type u} [inst : TopologicalSpace X],
  (∀ {Y : Type u} [inst_1 : TopologicalSpace Y] (f : X → Y),
      (∀ (K : Type u) [inst_2 : TopologicalSpace K] [CompactSpace K] [T2Space K] (g : K → X),
          Continuous g → Continuous (f ∘ g)) →
        Continuous f) →
    CompactlyGeneratedSpace 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

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpace