Theorems · Definition · general topology

CompactlyGeneratedSpace

(X : Type u) → [TopologicalSpace X] → Prop

A topological space X is compactly generated if its topology is finer than (and thus equal to) the compactly generated topology, i.e. it is coinduced by the continuous maps from compact Hausdorff spaces to X. In this version, intended for topological purposes, the compact spaces are taken in the same universe as X. See UCompactlyGeneratedSpace for a version with an explicit universe parameter, intended for categorical purposes.

Defined in

Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Cited by

18 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

TopologicalSpace