LemmaStatement: Literature-sourcedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)verified 2026-07-29 (claude-fable-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 open set containing a point contains an open set containing it whose closure is compact and still inside; such a space is regular

Statement

Let $X$ be a locally compact (Locally compact topological space: every point has a compact neighbourhood; and what this says in a metric space) Hausdorff (Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not) space, so that every point of $X$ has a compact neighbourhood (Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open, Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right). Closures are taken in $X$ unless a subscript names another space (Interior, closure, boundary, exterior, derived set and isolated point in a topological space). Then:

Shrinking with a compact closure. For every $x \in X$ and every open $U \subseteq X$ with $x \in U$ there is an open $V \subseteq X$ with $x \in V \subseteq \overline{V} \subseteq U$ and $\overline{V}$ compact.
A base. The family of open subsets of $X$ whose closure is compact is a basis for the topology of $X$ (Basis and subbasis for a topology, and the topology generated by a family of sets).
Regularity. $X$ is regular (Regular spaces and $T_3$ spaces, with the source disagreement over whether regularity includes $T_1$ stated explicitly).

Nothing stronger than regularity is claimed: complete regularity of such a space is a separate statement, needs a continuous real-valued function, and is not proved here.

Facts & Assumptions

Given: A locally compact Hausdorff space $X$ , a point $x \in X$ and an open set $U \subseteq X$ with $x \in U$ .

[A1]

Every point of $X$ has a compact neighbourhood: for each $x$ there are a compact subset $K \subseteq X$ and an open $O \subseteq X$ with $x \in O \subseteq K$ (Locally compact topological space: every point has a compact neighbourhood; and what this says in a metric space, Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open, Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right).

[A2]

$X$ is Hausdorff: 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).

[A3]

$\operatorname{int}(K)$ is the largest open subset of $K$ , and $\overline{A}$ is the smallest closed superset of $A$ (Interior, closure, boundary, exterior, derived set and isolated point in a topological space, Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison).

[L1]

For $S \subseteq X$ the open sets of the subspace $S$ are the traces $U' \cap S$ of the open sets of $X$ ; an open subset of $X$ contained in $S$ is open in $S$ ; and for $S \subseteq T \subseteq X$ the topology $S$ inherits from $T$ is the topology it inherits from $X$ (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]

A compact subset of a Hausdorff space is closed (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).

[L3]

A compact Hausdorff space is regular (A compact Hausdorff space is regular and normal, hence $T_3$ and $T_4$ , claim 1).

[L4]

A space is regular if and only if for every point $p$ of it and every set $W$ open in it with $p \in W$ there is a set $V$ open in it with $p \in V \subseteq \operatorname{cl}(V) \subseteq W$ , the closure being taken in that space (A space is regular if and only if every point has a neighbourhood base of closed neighbourhoods, if and only if $x \in U$ open gives an open $V$ with $x \in V \subseteq \overline{V} \subseteq U$ , (a) iff (b), Regular spaces and $T_3$ spaces, with the source disagreement over whether regularity includes $T_1$ stated explicitly).

[L5]

For $S \subseteq X$ and $A \subseteq S$ one has $\operatorname{cl}_S(A) = \overline{A} \cap S$ (For $A \subseteq S \subseteq X$ the closure of $A$ in $S$ is $\overline{A}^{X} \cap S$ , while the interior only contains $\operatorname{int}^{X}(A) \cap S$ , with equality when $S$ is open; and a dense subset of $X$ traces to a dense subset of every open $S$ , claim 1).

[L6]

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

[L7]

A family of open sets is a basis for the topology exactly when for every open $W$ and every $p \in W$ some member of the family contains $p$ and is contained in $W$ (Basis and subbasis for a topology, and the topology generated by a family of sets).

Proof

technique · direct

1.1

By [A1] fix a compact $K \subseteq X$ and an open $O \subseteq X$ with $x \in O \subseteq K$ ; then $O \subseteq \operatorname{int}(K)$ by [A3], so $x \in \operatorname{int}(K)$ .

A1A3choose

1.2

The subspace $K$ is Hausdorff: distinct $p, q \in K$ have disjoint open $U_1 \ni p$ and $U_2 \ni q$ in $X$ by [A2], and the traces $U_1 \cap K$ and $U_2 \cap K$ are disjoint open sets of the subspace containing $p$ and $q$ respectively.

A2L1

1.3

$K$ is closed in $X$ , being a compact subset of the Hausdorff space $X$ .

A2L2

2.1

The subspace $K$ is compact and Hausdorff, hence regular.

step 1.2L3

2.2

Put $G := U \cap \operatorname{int}(K)$ ; it is open in $X$ , contains $x$ by step 1.1, is contained in $K$ by [A3], and is therefore also open in the subspace $K$ .

step 1.1A3L1

3.1

Applying [L4] inside the space $K$ , which is regular by step 2.1, to the point $x$ and the set $G$ open in $K$ , there is a set $V$ open in $K$ with $x \in V \subseteq \operatorname{cl}_K(V) \subseteq G$ .

step 2.1step 2.2L4choose

4.1

$V$ is open in $X$ : by [L1] there is an open $V' \subseteq X$ with $V = V' \cap K$ , and since $V \subseteq G \subseteq \operatorname{int}(K)$ we get $V = V \cap \operatorname{int}(K) = V' \cap K \cap \operatorname{int}(K) = V' \cap \operatorname{int}(K)$ , an intersection of two open subsets of $X$ .

step 2.2step 3.1L1A3

4.2

$\overline{V} = \operatorname{cl}_K(V)$ : from $V \subseteq K$ and $K$ closed in $X$ (step 1.3) the smallest closed superset of $V$ satisfies $\overline{V} \subseteq K$ , and [L5] gives $\operatorname{cl}_K(V) = \overline{V} \cap K = \overline{V}$ .

step 1.3step 3.1A3L5

5.1

$\overline{V}$ is compact: by step 4.2 it is $\operatorname{cl}_K(V)$ , which is closed in the compact subspace $K$ and hence compact by [L6]; and by the transitivity clause of [L1] the topology it inherits from $K$ is the one it inherits from $X$ , so it is a compact subset of $X$ .

step 4.2L1L6

6.1

Combining, $V$ is open in $X$ by step 4.1, $x \in V \subseteq \overline{V} = \operatorname{cl}_K(V) \subseteq G \subseteq U$ by steps 3.1, 4.2 and 2.2, and $\overline{V}$ is compact by step 5.1; as $x$ and $U$ were arbitrary this is claim 1.

step 2.2step 3.1step 4.1step 4.2step 5.1

7.1

The open subsets of $X$ with compact closure are open, and by step 6.1 every open $U$ and every $x \in U$ admit such a set $V$ with $x \in V \subseteq U$ ; so by [L7] they form a basis for the topology of $X$ , which is claim 2.

step 6.1L7

7.2

Step 6.1 gives, for every $x$ and every open $U \ni x$ , an open $V$ with $x \in V \subseteq \overline{V} \subseteq U$ , which is condition (b) of [L4] for the space $X$ ; hence $X$ is regular, which is claim 3.

step 6.1L4

8.1

Steps 6.1, 7.1 and 7.2 are claims 1, 2 and 3, so the lemma is proved.

step 6.1step 7.1step 7.2∎

Remarks

Which clause of local compactness is used. Only that every point has a compact neighbourhood, in the weak sense of Locally compact topological space: every point has a compact neighbourhood; and what this says in a metric space: a compact $K$ with $x$ in its interior. The stronger-sounding conclusion, a neighbourhood base of open sets with compact closure, is derived from it here, and the Hausdorff hypothesis is what makes the derivation possible — it is used twice, once to make $K$ closed in $X$ and once to make the subspace $K$ regular.
Why the argument moves into the subspace $K$ and back out. Regularity is available inside $K$ , because $K$ is compact Hausdorff, and not yet available in $X$ — proving it for $X$ is claim 3. The two transfers back to $X$ are step 4.1, which uses that $V$ sits inside the open set $\operatorname{int}(K)$ , and step 4.2, which uses that $K$ is closed. Neither transfer works without its hypothesis: an open set of a subspace need not be open in the ambient space, and a closure computed in a subspace need not agree with the ambient closure.
Compactness of $\overline{V}$ , not merely of its closure inside $K$ . Compactness is a property of a space, and $\overline{V}$ carries the same topology whether it is reached through $K$ or directly from $X$ (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); step 5.1 records that, so no second notion of "compact subset" is created.

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: 97 results over 18 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)
Regular space (Wikipedia) (standard reference, not scraped)
B. McKay, Topology Lecture Notes (standard reference, not scraped)