TheoremStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (claude-sonnet-5 + deepseek-v4-pro)verified 2026-08-05 (claude-sonnet-5)

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.

In a locally compact Hausdorff space every point has a neighbourhood base of compact sets, every open subspace and every closed subspace is locally compact, every open set around a point contains an open set with compact closure inside it, and every compact set sits inside an open set with compact closure

Statement

Let $(X, \mathcal{T})$ be a topological space (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison). Then:

A neighbourhood base of compact sets. If $X$ is locally compact (Locally compact topological space: every point has a compact neighbourhood; and what this says in a metric space) and Hausdorff (Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not), then every neighbourhood $N$ of a point $x \in X$ (Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open) contains a compact neighbourhood of $x$ ; so the compact neighbourhoods of $x$ form a neighbourhood base at $x$ .
Heredity along open and closed subspaces. If $X$ is locally compact and Hausdorff and $S \subseteq X$ is open, then the subspace $S$ is locally compact (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). If $X$ is locally compact and $F \subseteq X$ is closed, then the subspace $F$ is locally compact; no Hausdorff hypothesis is used for this half.
Shrinking inside an open set. If $X$ is locally compact and Hausdorff, $O \subseteq X$ is open and $x \in O$ , there is an open $V$ with $x \in V \subseteq \overline{V} \subseteq O$ and $\overline{V}$ a compact subset of $X$ .
Compact sets sit in open sets with compact closure. If $X$ is locally compact and Hausdorff and $K \subseteq X$ is compact, there is an open $V \subseteq X$ with $K \subseteq V$ and $\overline{V}$ a compact subset of $X$ (Interior, closure, boundary, exterior, derived set and isolated point in a topological space).

No choice principle is used; every cover produced below is defined by a formula and thinned by A subspace is compact exactly when every family of open subsets of the ambient space covering it, indexed or not, has finitely many members covering it, which returns members rather than indices.

Facts & Assumptions

Given: A topological space $(X, \mathcal{T})$ .

[L1]

$X$ is locally compact when every point has a compact neighbourhood; a subset $A$ is a compact subset when the subspace it carries is compact (Locally compact topological space: every point has a compact neighbourhood; and what this says in a metric space, Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right, 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).

[L2]

$X$ is Hausdorff when distinct points have disjoint open neighbourhoods (Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not).

[L3]

In a Hausdorff space a compact subset is closed, and a point outside a compact subset is separated from it by disjoint open sets (In a Hausdorff space a point and a disjoint compact set, and two disjoint compact sets, have disjoint open neighbourhoods; hence every compact subset is closed, and in a compact Hausdorff space the compact subsets are exactly the closed ones, claims 1 and 3).

[L4]

A closed subset of a compact space is a compact subset of it, and a finite union of compact subsets is compact (A closed subspace of a compact space is compact, and a finite union of compact subspaces is compact).

[L5]

$\overline{A}$ is the smallest closed superset of $A$ , so $\overline{A} \subseteq F$ for every closed $F \supseteq A$ , and $A$ is closed exactly when $A = \overline{A}$ ; $\operatorname{int}(A)$ is the largest open subset of $A$ , and $x \in \operatorname{int}(A)$ exactly when $A$ is a neighbourhood of $x$ (Interior, closure, boundary, exterior, derived set and isolated point in a topological space, A point lies in the closure of $A$ iff every basic neighbourhood of it meets $A$ ; the closure is the smallest closed superset and equals $A$ together with its derived set, claim 2).

[L6]

The open sets of a subspace $S$ are the traces $U \cap S$ of the open sets of $X$ and its closed sets are the traces of the closed sets; and for $A \subseteq S \subseteq X$ the topology $A$ inherits from $S$ is the one it inherits from $X$ , so compactness of $A$ does not depend on which of the two it is read in (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, Hereditary, open-hereditary and closed-hereditary properties of topological spaces).

[L7]

An open set is a neighbourhood of each of its points, a superset of a neighbourhood of $x$ is a neighbourhood of $x$ , and a union of finitely many closed sets is closed (Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open, Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison).

[L8]

$A$ is a compact subset of $X$ exactly when every family of open subsets of $X$ covering $A$ has finitely many members covering $A$ , or else $A = \varnothing$ (A subspace is compact exactly when every family of open subsets of the ambient space covering it, indexed or not, has finitely many members covering it, claim 1).

Proof

technique · direct

1.1

For claim 1 let $X$ be locally compact and Hausdorff, let $x \in X$ and let $N$ be a neighbourhood of $x$ ; fix a compact neighbourhood $K$ of $x$ and open sets $U, V$ with $x \in U \subseteq K$ and $x \in V \subseteq N$ , and put $W := U \cap V$ , an open set with $x \in W \subseteq K \cap N$ . By [L3] the compact set $K$ is closed.

L1L2L3L7construct

1.2

For the closed half of claim 2 let $X$ be locally compact, let $F \subseteq X$ be closed and let $x \in F$ ; a compact neighbourhood $K$ of $x$ in $X$ contains an open $U \ni x$ , and $K \cap F$ is the trace of the closed $F$ on $K$ , hence closed in the subspace $K$ and so a compact subset by [L4] and [L6], while $x \in U \cap F \subseteq K \cap F$ with $U \cap F$ open in $F$ exhibits $K \cap F$ as a neighbourhood of $x$ in the subspace $F$ . So $F$ is locally compact.

L1L4L6L7

2.1

The set $F_0 := K \setminus W = K \cap (X \setminus W)$ is the trace of a closed set on $K$ , hence closed in the subspace $K$ and a compact subset of $X$ by [L4] and [L6]; and $x \notin F_0$ , since $x \in W$ .

L4L6step 1.1

3.1

By [L3] there are disjoint open sets $A \ni x$ and $B \supseteq F_0$ ; put $G := A \cap W$ , an open set with $x \in G$ .

L3step 1.1step 2.1

4.1

$G \subseteq K$ and $K$ is closed, so $\overline{G} \subseteq K$ by [L5]; and $G \subseteq A \subseteq X \setminus B$ , a closed set, so $\overline{G} \subseteq X \setminus B$ . Hence $\overline{G} \subseteq K \setminus B \subseteq K \setminus F_0 = K \cap W \subseteq W \subseteq N$ .

L5L7step 1.1step 3.1

5.1

$\overline{G}$ is closed and contained in $K$ , so it is the trace of a closed set on $K$ , closed in the subspace $K$ , and a compact subset of $X$ by [L4] and [L6]; and it is a neighbourhood of $x$ by [L7], since the open $G$ satisfies $x \in G \subseteq \overline{G}$ . With step 4.1 it lies inside $N$ , so claim 1 holds.

L4L6L7step 4.1

6.1

For the open half of claim 2 let $S \subseteq X$ be open and let $x \in S$ ; then $S$ is a neighbourhood of $x$ by [L7], so claim 1 supplies a compact neighbourhood $C$ of $x$ in $X$ with $C \subseteq S$ . An open $U$ of $X$ with $x \in U \subseteq C$ satisfies $U \subseteq S$ , so $U = U \cap S$ is open in $S$ and $C$ is a neighbourhood of $x$ in the subspace $S$ ; and by [L6] compactness of $C$ read in $S$ is compactness read in $X$ . So $S$ is locally compact and claim 2 is proved.

L1L6L7step 5.1

6.2

For claim 4 put $\mathcal{V} := \{\, U \in \mathcal{T} : \overline{U} \text{ is a compact subset of } X \,\}$ , a family cut out by a property. It covers $X$ : given $y \in X$ , claim 1 applied with $N := X$ gives a compact neighbourhood $C$ of $y$ , which is closed by [L3], and an open $U$ with $y \in U \subseteq C$ ; then $\overline{U} \subseteq C$ by [L5], $\overline{U}$ is closed in the subspace $C$ by [L6], and [L4] makes it a compact subset of $X$ , so $U \in \mathcal{V}$ .

L3L4L5L6step 5.1construct

6.3

For claim 3 let $O$ be open and $x \in O$ ; then $O$ is a neighbourhood of $x$ by [L7], so claim 1, proved at step 5.1, gives a compact neighbourhood $C$ of $x$ with $C \subseteq O$ , and $C$ is closed by [L3]. Put $V := \operatorname{int}(C)$ , which is open and contains $x$ by [L5], $C$ being a neighbourhood of $x$ ; then $V \subseteq C$ gives $\overline{V} \subseteq \overline{C} = C \subseteq O$ by [L5], and $\overline{V}$ is a closed subset of the compact $C$ , hence closed in the subspace $C$ by [L6] and a compact subset of $X$ by [L4]. So $x \in V \subseteq \overline{V} \subseteq O$ with $\overline{V}$ compact, which is claim 3.

L3L4L5L6L7step 5.1

7.1

Let $K \subseteq X$ be compact. If $K = \varnothing$ then $V := \varnothing$ has $\overline{V} = \varnothing$ compact; otherwise [L8] gives $n \in \mathbb{N}$ and $U_0, \dots, U_n \in \mathcal{V}$ with $K \subseteq U_0 \cup \dots \cup U_n =: V$ , an open set.

L8step 6.2

8.1

The set $\overline{U_0} \cup \dots \cup \overline{U_n}$ is closed by [L7] and contains $V$ , so $\overline{V}$ is contained in it by [L5]; that union is a compact subset by [L4], and $\overline{V}$ is a closed subset of it, hence closed in the subspace it carries and compact by [L4] and [L6]. So $K \subseteq V$ with $\overline{V}$ compact, which is claim 4; claims 1, 2 and 3 were proved at steps 5.1, 6.1 with 6.2, and 6.3.

L4L5L6L7step 6.3step 7.1∎

Remarks

Where the Hausdorff hypothesis is spent. Twice, and both times through In a Hausdorff space a point and a disjoint compact set, and two disjoint compact sets, have disjoint open neighbourhoods; hence every compact subset is closed, and in a compact Hausdorff space the compact subsets are exactly the closed ones: to know that the compact neighbourhood $K$ is closed, and to separate the point $x$ from the compact $K \setminus W$ . Without it the compact neighbourhood cannot be shrunk, and claim 1 is exactly the shrinking.

Claim 3 is the form the rest of the library asks for. "Every neighbourhood contains a compact neighbourhood" and "every open set around a point contains an open $V$ with $\overline{V}$ compact inside it" are the same statement in different clothes, and the second is the one a nested-shrinking construction needs, since it hands back an open set whose closure is already inside the target. It is used in Assuming dependent choice, every locally compact Hausdorff space is a Baire space.

Claim 2 splits into two halves of different strength. The closed half is true in any locally compact space and its proof is three lines; the open half runs through claim 1 and therefore through the Hausdorff hypothesis. Together they do not give heredity: an arbitrary subspace of a locally compact Hausdorff space need not be locally compact, and FALSE: every subspace of a locally compact space is locally compact carries the witness.

Claim 4 pads a compact set, not a point. It says a compact set can always be padded to an open set that is still "bounded" in the only sense available here, namely having compact closure. Separating a single point of $X$ from the added point $\infty$ costs less than that: $X^{*}$ is compact and contains $X$ as an open subspace; $X$ is dense in $X^{*}$ exactly when $X$ is not compact; and $X^{*}$ is Hausdorff exactly when $X$ is locally compact and Hausdorff does it at step 1.4 from claim 1 alone, taking a compact neighbourhood of the point and using that it is closed.

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 87 results over 17 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

Locally compact space (Wikipedia) (standard reference, not scraped)
J. Munkres, Topology, 2nd ed., §29 (standard reference, not scraped)
Stacks Project, Tag 08ZQ (standard reference, not scraped)
I. Khatchatourian, Compactifications (MAT327 notes) (standard reference, not scraped)