English
If X has a topology t and X is UCompactlyGeneratedSpace, then t equals the compactly generated topology on X.
Русский
Если у X есть топология t и X — UCompactlyGeneratedSpace, то t совпадает с компакто-генерируемой топологией на X.
LaTeX
$$$ [t : TopologicalSpace X] [\text{UCompactlyGeneratedSpace}(X)] \Rightarrow t = \operatorname{compactlyGenerated}(X) $$$
Lean4
/-- The compactly generated topology on a topological space `X`. This is the finest topology
which makes all maps from compact Hausdorff spaces to `X`, which are continuous for the original
topology, continuous.
Note: this definition should be used with an explicit universe parameter `u` for the size of the
compact Hausdorff spaces mapping to `X`.
-/
def compactlyGenerated (X : Type w) [TopologicalSpace X] : TopologicalSpace X :=
let f : (Σ (i : (S : CompHaus.{u}) × C(S, X)), i.fst) → X := fun ⟨⟨_, i⟩, s⟩ ↦ i s
coinduced f inferInstance
