All compact subsets form a CG-cover

Proved

QAlgorithms.Papers.Independent.Intakethird100.P32.allCompactSubsets_isCGCover

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $X$ be a compactly generated Hausdorff space. Index a family by all compact subsets $K\subseteq X$ , with each member the inclusion $K\hookrightarrow X$ . Then

\{K\hookrightarrow X\mid K\subseteq X\text{ compact}\}\text{ is a }\mathcal{CG}\text{-cover}.

No exhaustion or countability choice is required. This supplies the compact-subset covering family used throughout the paper, also for the empty space.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P32

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P32

universe u

open Set Topology

/-- Corollary 3.1, PDF p.18: the inclusion family of all compact subsets covers
any CGH space in the CG topology, including the empty space. -/
theorem allCompactSubsets_isCGCover (X : Type u) [TopologicalSpace X]
    [T2Space X] [CompactlyGeneratedSpace X] : CGCover (allCompactSubsets X) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P32

Source

Compactly Generated Stacks: A Cartesian Closed Theory of Topological Stacks, arXiv:0907.3925v3, PDF p. 18, Corollary 3.1

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

For every Hausdorff, compactly generated topological space $X$ , consider the family indexed by all compact subsets $C\subseteq X$ , whose member at index $C$ is $C$ itself. For every compact subset $K\subseteq X$ , there exists a finite set $J$ of such compact subsets of $X$ satisfying

K=\bigcup_{C\in J}\operatorname{int}_K(K\cap C),

where interiors are taken in the subspace topology on $K$ . Equivalently, each point of $K$ lies in the relative interior of its intersection with at least one compact set selected by $J$ . Empty compact subsets are included among the indices, $K$ may be empty, and for empty $K$ the finite set $J$ may be empty.

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph