PropositionStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-31

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Every closed subspace of a paracompact space is paracompact

Statement

Every closed subspace of a paracompact topological space is paracompact.

Facts & Assumptions

Given: A paracompact space $X$ , a closed subset $A\subseteq X$ , and an open cover $\mathcal U$ of the subspace $A$ .

[F1]

An open subset of $A$ has the form $O\cap A$ for an open $O\subseteq X$ , and $X\setminus A$ is open (Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace).

[F2]

Every open cover of $X$ has a locally finite open refining cover (Paracompactness: every open cover has a locally finite open refinement, with no separation axiom built into the word).

Proof

technique · direct

1.1

For each member of $\mathcal U$ , take all ambient open $O$ whose trace $O\cap A$ is that member; together with $X\setminus A$ , these ambient open sets form an open cover $\mathcal W$ of $X$ .

F1construct

1.2

By [F2], fix a locally finite open cover $\mathcal V$ refining $\mathcal W$ .

F2choose

2.1

The nonempty traces $V\cap A$ for $V\in\mathcal V$ cover $A$ , are open in $A$ , and refine $\mathcal U$ : a $V$ meeting $A$ cannot be contained in $X\setminus A$ , so its containing member of $\mathcal W$ is an ambient representative of a member of $\mathcal U$ .

F1step 1.1step 1.2

2.2

These traces are locally finite in $A$ , because the trace on $A$ of a neighbourhood in $X$ meeting only finitely many $V$ meets only the corresponding finitely many traces.

step 1.2F1

3.1

The family in step 2.1 is therefore the locally finite open refinement required for $A$ , so $A$ is paracompact.

step 2.1step 2.2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 17 results over 11 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

J. Robbin, Partitions of Unity (standard reference, not scraped)
R. Gardner, Notes on Munkres Section 41: Paracompactness (East Tennessee State University) (standard reference, not scraped)