Alphabeta Math
DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (z-ai/glm-5.2)audited 2026-07-27
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.

Countably compact, sequentially compact and limit point compact metric spaces

Definition

Let (X,d) be a metric space (Metric space: d(x,y)=0 iff x=y, symmetry, and the triangle inequality; pseudometric and ultrametric), with open sets as in 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 and open covers, subcovers, finiteness and compactness as in Open cover, subcover, compact metric space, and compact subset of a metric space.

A subset A⊆X is called countably compact, sequentially compact or limit point compact when the metric subspace (A,dA) is (Isometry, isometric embedding, and the subspace metric on a subset), exactly as for compactness.

The countable covers may be listed. A nonempty at most countable family U admits a surjection N→U (A nonempty set is at most countable iff it is a surjective image of N), so countable compactness says: for every sequence (Un)n∈N of open sets with X=⋃n∈NUn there are finitely many indices whose sets already cover X. That surjection is produced from the countability assumption alone and no choice principle is involved; the empty family covers only the empty space, which is compact anyway.

Limit points are computed where the set lives. For S⊆A⊆X and a∈A, the identity BA(a,r)=BX(a,r)∩A (Isometry, isometric embedding, and the subspace metric on a subset) shows that a is a limit point of S in the subspace (A,dA) exactly when a is a limit point of S in X and lies in A. So "A is limit point compact" says that every infinite S⊆A has a limit point belonging to A; a limit point outside A does not count, and that is what distinguishes the property from a statement about X.

Remarks

Three conditions, and none of them is compactness by definition. Each of the three weakens or replaces the open-cover condition of Open cover, subcover, compact metric space, and compact subset of a metric space: countable compactness restricts the covers tested, sequential compactness speaks about sequences instead of covers, and limit point compactness speaks about subsets. That the four conditions are not equivalent for topological spaces in general is standard and is quoted from the references, not proved here. For metric spaces they do coincide, but the coincidence is a theorem with a choice cost that varies from implication to implication, and it is proved on this page one arrow at a time (In any metric space compactness implies countable compactness and limit point compactness, and each of countable compactness and limit point compactness implies sequential compactness; every implication here is proved without a choice principle, For a metric space, compact, countably compact, limit point compact, sequentially compact, and complete together with totally bounded are all equivalent, given countable choice and dependent choice, What each implication between the compactness properties of a metric space costs: which are theorems of ZF, which use countable choice, and which use dependent choice).

Indexing starts at 0. A sequence here is a function on N and N contains 0 (Sequences of reals: bounded, eventually, frequently, tails, subsequences), so a subsequence is (xnj)j∈N with n0<n1<⋯ and nj≥j (A strictly increasing index map satisfies nk≥k). Every recursive construction of a subsequence on this page produces n0 first and then nj+1>nj, and every radius written 1/(j+1) is written that way because 1/j is undefined at j=0.

Depends on

Used by

Dependency tree · two levels

38 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources