English
A topological space X is compactly generated if its topology is the coinduced topology from all continuous maps from compact Hausdorff spaces into X.
Русский
Топология пространства X является компактно-генерированной, если она сопряжена с помощьюобразующими топологиями из компактных Hausdorff-пространств в X.
LaTeX
$$$\\mathrm{CompactlyGeneratedSpace}(X)$$$
Lean4
/-- 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.
-/
abbrev CompactlyGeneratedSpace (X : Type u) [TopologicalSpace X] : Prop :=
UCompactlyGeneratedSpace.{u} X
