Open covers are CG-covers

Proved

QAlgorithms.Papers.Independent.Intakethird100.P32.openCover_isCGCover

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

prove2quantum

Let $X$ be a compactly generated Hausdorff space and $(U_a)_{a\in A}$ a universe-small open cover. Then $(U_a\hookrightarrow X)_{a\in A}$ is a $\mathcal{CG}$ -cover. Explicitly, for every compact subset $K\subseteq X$ , there is a finite set $J\subseteq A$ such that

K=\bigcup_{a\in J}\operatorname{int}_{K}(K\cap U_a).

This is the inclusion of ordinary open covers into the compactly generated covering families of Definition 3.1.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P32

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P32

universe u

open Set Topology

/-- Proposition 3.2, PDF p.18: every open cover of a CGH space is a CG-cover. -/
theorem openCover_isCGCover (X : Type u) [TopologicalSpace X]
    [T2Space X] [CompactlyGeneratedSpace X] {A : Type u} (U : A → Set X)
    (hU : IsOpenCover U) : CGCover U := 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, Proposition 3.2

Read-back

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

For every Hausdorff, compactly generated topological space $X$ , every index type $A$ in the same universe, and every family $(U_a)_{a\in A}$ of open subsets covering $X$ , the following holds: for every compact subset $K\subseteq X$ , there exists a finite subset $J\subseteq A$ such that

K=\bigcup_{a\in J}\operatorname{int}_K(K\cap U_a).

Here $K$ has its subspace topology, $K\cap U_a$ is viewed as a subset of $K$ , and $\operatorname{int}_K$ denotes interior in that subspace. Thus every point of $K$ belongs to the relative interior of at least one selected member. The compact set $K$ may be empty, in which case $J=\varnothing$ is permitted; no nonemptiness of $X$ , $A$ , or the cover members is assumed.

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