Paracompact Hausdorff spaces admit shrinkings

Proved

QAlgorithms.Papers.Independent.Intakethird100.P32.paracompactHausdorff_isShrinkingSpace

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

prove2quantum

Let $X$ be a paracompact Hausdorff space, and let $(U_a)_{a\in A}$ be any universe-small open cover. There is an open cover $(V_a)_{a\in A}$ , indexed by the same set, such that

\overline{V_a}\subseteq U_a\qquad(a\in A).

Thus every paracompact Hausdorff space is a shrinking space. Empty spaces and empty covers are included.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P32

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P32

universe u

open Set Topology

/-- Proposition 2.2, PDF p.12: every paracompact Hausdorff space is a shrinking
space. This is the general ordinary-topology fact explicitly recalled on that page. -/
theorem paracompactHausdorff_isShrinkingSpace (X : Type u) [TopologicalSpace X]
    [T2Space X] [ParacompactSpace X] : ShrinkingSpace 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. 12, Proposition 2.2

Read-back

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

For every Hausdorff, paracompact topological space $X$ , every index type $A$ in the same universe as $X$ , and every family $(U_a)_{a\in A}$ of open subsets of $X$ satisfying $\bigcup_{a\in A}U_a=X$ , there exists a family $(V_a)_{a\in A}$ of open subsets of $X$ such that

\bigcup_{a\in A}V_a=X \qquad\text{and}\qquad \overline{V_a}\subseteq U_a\quad\text{for every }a\in A,

where closures are taken in $X$ . The new family uses exactly the same index type. Empty spaces and empty members of either family are allowed; an empty index type satisfies the covering hypothesis precisely when $X$ is 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