Alphabeta Math
DefinitionDefinition: AI-adaptedProof: Not applicableSession-authored (Fable 5 assisted)verified 2026-08-05 (gpt-5.6-sol-codex-subscription)
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.

Locally compact topological space: every point has a compact neighbourhood; and what this says in a metric space

Definition

A topological space (X,T)(X, \mathcal{T}) (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison) is locally compact when

every point of XX has a compact neighbourhood:

that is, for every xXx \in X there is a neighbourhood NN of xx (Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open) that is a compact subset of XX (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).

A neighbourhood need not be open here, and that is what makes the condition the weak one it is meant to be: NN is required only to contain some open set containing xx. Writing "compact open neighbourhood" instead would define a strictly stronger property, satisfied by no space in which a point has no compact open neighbourhood, R\mathbb{R} among them; and requiring the compact set merely to contain xx would define a property so weak that every space with a singleton has it, singletons being compact.

Every compact space is locally compact, since XX itself is a neighbourhood of each of its points and is a compact subset of itself. The converse fails, and Rn\mathbb{R}^n is the standard witness.

What the condition says in a metric space. Let (X,d)(X,d) be a metric space carrying its metric topology (The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement, Metrizable space: a topological space whose topology is induced by some metric; metrizability is topological, the metric is not), with balls as in Open ball, closed ball and sphere in a metric space, and let xXx \in X. Then

xx has a compact neighbourhood if and only if there are a real r>0r > 0 and a compact KXK \subseteq X with B(x,r)KB(x,r) \subseteq K.

Both directions are immediate and are discharged here. If NN is a compact neighbourhood of xx, fix an open UU with xUNx \in U \subseteq N; by The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement there is r>0r > 0 with B(x,r)UNB(x,r) \subseteq U \subseteq N, so K:=NK := N serves. Conversely, if B(x,r)KB(x,r) \subseteq K with KK compact, then KK contains the open set B(x,r)B(x,r), which contains xx, so KK is a neighbourhood of xx and is compact. Compactness of a subset of (X,d)(X,d) means the same thing read metrically and read topologically (For a metric space with its metric topology, compactness in the topological sense is compactness in the metric sense, and the two notions of compact subset coincide), so the criterion may be applied with either development's theorems.

Rn\mathbb{R}^n is locally compact for every n1n \ge 1. Give Rn\mathbb{R}^n the product topology, which is the metric topology of the Euclidean metric d2d_2 (Rn\mathbb{R}^n as the set of functions nRn \to \mathbb{R}, and d1d_1, d2d_2, dd_\infty are metrics on it, A subset of Rn\mathbb{R}^n with the product topology is compact exactly when it is closed and bounded, the product topology being the Euclidean metric topology). For pRnp \in \mathbb{R}^n the set

Qp  :=  {xRn:d2(x,p)1}Q_p \;:=\; \{\, x \in \mathbb{R}^n : d_2(x,p) \le 1 \,\}

is closed, being the complement of the union of the open balls B(y,d2(y,p)1)B(y, d_2(y,p) - 1) over the points yy with d2(y,p)>1d_2(y,p) > 1, and it is bounded (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space), lying inside B(p,2)B(p, 2); so QpQ_p is compact by A subset of Rn\mathbb{R}^n with the product topology is compact exactly when it is closed and bounded, the product topology being the Euclidean metric topology. It contains the open ball B(p,1)B(p,1), which contains pp, so it is a compact neighbourhood of pp. The space Rn\mathbb{R}^n is not compact, so local compactness is strictly weaker than compactness.

Remarks

Local compactness is a local condition and compactness is not. The definition quantifies over points and asks for something in a neighbourhood of each; nothing is asserted about covers of the whole space. That is why a locally compact space may be as large as one likes, and why the two properties separate.

Where the extra strength is needed. For an arbitrary space, "every point has a compact neighbourhood" does not by itself give a base of compact neighbourhoods at each point, nor an open set with compact closure around each compact set. Both of those do follow once the space is also Hausdorff, and that is 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; several authors build the stronger condition into the definition and then note the agreement in the Hausdorff case. This library takes the weak definition and proves the strengthening under the hypothesis that licenses it.

Local compactness is not hereditary, unlike metrizability. A subspace of a locally compact space need not be locally compact, and FALSE: every subspace of a locally compact space is locally compact records the failure with a witness; what does survive is heredity along open and along closed subspaces of a locally compact Hausdorff space (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).

Depends on

Used by

Dependency tree · next 3 levels

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