Theorems · Inductive type · general topology

UCompactlyGeneratedSpace

(X : Type v) → [t : 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. This version includes an explicit universe parameter u which should always be specified. It is intended for categorical purposes. See CompactlyGeneratedSpace for the version without this parameter, intended for topological purposes.

Defined in

Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Cited by

12 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

TopologicalSpace