Theorems · Theorem · general topology

compactlyGeneratedSpace_of_isOpen

∀ {X : Type u} [inst : TopologicalSpace X],
  (∀ (s : Set X),
      (∀ (K : Type u) [inst_1 : TopologicalSpace K] [CompactSpace K] [T2Space K] (f : K → X),
          Continuous f → IsOpen (f ⁻¹' s)) →
        IsOpen s) →
    CompactlyGeneratedSpace X

A topological space X is compactly generated if a set s is open when f ⁻¹' s is open for every continuous map f : K → X, where K is compact Hausdorff.

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

TopologicalSpace