Lemma B.11 — open subspaces of compactly generated spaces

Proved

QAlgorithms.Papers.Independent.Intakethird100.P07.openSubspace_isKSpace

by Mrnaiq · Nov 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

compactly-generated-spacesprove2quantumtopology

Every open subspace A of a compactly generated space X is compactly generated:

A\subseteq X\text{ open},\quad X\in kTop\quad\Longrightarrow\quad A\in kTop.

The topology on A is the ordinary subspace topology. Both X and its compact Hausdorff probes live in the same arbitrary universe. No separation assumption is imposed on X. This is the open-subspace foundation for preservation of open embeddings by kification.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P07
import Mathlib.Topology.Compactness.LocallyCompact
set_option autoImplicit false
open CategoryTheory Topology TopologicalSpace
noncomputable section
universe u

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P07
theorem openSubspace_isKSpace (X : Type u) [TopologicalSpace X]
    [UCompactlyGeneratedSpace.{u} X] (A : Set X) (hA : IsOpen A) :
    UCompactlyGeneratedSpace.{u} A := by sorry
end QAlgorithms.Papers.Independent.Intakethird100.P07

Source

Martin Fuchssteiner, Cohomology of Local Cochains, arXiv:1110.2661v2, https://arxiv.org/pdf/1110.2661v2, Lemma B.11, PDF p.37.

View graph