Theorems · Theorem · general topology

uCompactlyGeneratedSpace_of_isOpen

∀ {X : Type w} [tX : TopologicalSpace X],
  (∀ (s : Set X), (∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsOpen (⇑f ⁻¹' s)) → IsOpen s) → UCompactlyGeneratedSpace 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 73 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpace