CG-covers on locally compact Hausdorff spaces admit open refinements

Proved

QAlgorithms.Papers.Independent.Intakethird100.P32.cgCover_hasOpenRefinement

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

prove2quantum

Let $X$ be a locally compact Hausdorff space, regarded in $\mathrm{CGH}$ , and let $(V_a\hookrightarrow X)_{a\in A}$ be a $\mathcal{CG}$ -cover. There is an open cover refining this family. Equivalently, its canonical interior refinement covers:

X=\bigcup_{a\in A}\operatorname{int}_{X}(V_a).

The refinement runs from open subsets into the given members $V_a$ . This identifies the covering behavior of the two topologies on locally compact Hausdorff spaces.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P32

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P32

universe u

open Set Topology

/-- Proposition 3.3, PDF p.18: every CG-cover of a locally compact Hausdorff
space admits an open refinement. The interiors give a canonical such refinement. -/
theorem cgCover_hasOpenRefinement (X : Type u) [TopologicalSpace X]
    [T2Space X] [CompactlyGeneratedSpace X] [LocallyCompactSpace X]
    {A : Type u} (V : A → Set X) (hV : CGCover V) :
    HasOpenRefinement V := 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.3

Read-back

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

For every Hausdorff, compactly generated, locally compact topological space $X$ , every index type $A$ in the same universe, and every family $(V_a)_{a\in A}$ of subsets of $X$ , suppose that for each 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 V_a),

with interiors taken in the subspace $K$ . Then

X=\bigcup_{a\in A}\operatorname{int}_X(V_a).

In particular, every point of $X$ lies in the interior in $X$ of some original family member; the members $V_a$ themselves are not assumed open. Empty spaces and empty family members are allowed. The hypothesis for $K=\varnothing$ permits $J=\varnothing$ , and if $X=\varnothing$ , the conclusion has no points to check.

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