Alphabeta Math
DefinitionDefinition: AI-adaptedProof: Not applicableSession-authored (Fable 5 assisted)judge 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.

Open cover, subcover, compact metric space, and compact subset of a metric space

Definition

Let (X,d)(X,d) be a metric space (Metric space: d(x,y)=0d(x,y) = 0 iff x=yx = 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 balls as in Open ball, closed ball and sphere in a metric space.

  • An open cover of (X,d)(X,d) is a family U\mathcal{U} of open subsets of XX with X=UX = \bigcup \mathcal{U}, where U={xX:xU for some UU}\bigcup \mathcal{U} = \{\, x \in X : x \in U \text{ for some } U \in \mathcal{U} \,\}.
  • A subcover of U\mathcal{U} is a subfamily VU\mathcal{V} \subseteq \mathcal{U} that is itself an open cover.
  • A family V\mathcal{V} of sets is finite when V=\mathcal{V} = \emptyset or there are nNn \in \mathbb{N} and sets V0,,VnV_0, \dots, V_n with V={V0,,Vn}\mathcal{V} = \{V_0, \dots, V_n\}; repetitions in the list are allowed and harmless.
  • (X,d)(X,d) is compact when every open cover of it has a finite subcover: for every open cover U\mathcal{U}, either X=X = \emptyset and the empty subfamily covers it, or there are nNn \in \mathbb{N} and U0,,UnUU_0, \dots, U_n \in \mathcal{U} with X=U0Un.X = U_0 \cup \dots \cup U_n .
  • A subset AXA \subseteq X is a compact subset of XX when the metric subspace (A,dA)(A, d_A) is a compact metric space, dAd_A being the restriction of dd to A×AA \times A (Isometry, isometric embedding, and the subspace metric on a subset).

Compactness of a subset is defined intrinsically, and only intrinsically. The last clause speaks about the subspace (A,dA)(A,d_A) and its own open sets, not about families of open subsets of the ambient XX. The two readings do agree, but that is a theorem and not a convention: it is A subset of a metric space is open in the subspace metric exactly when it is the trace of an open set of the ambient space, and it is compact as a metric space in its own right exactly when every family of open subsets of the ambient space covering it, indexed or not, has finitely many members covering it, and no item of this library may use the ambient reading without citing it. Taking the intrinsic reading as the definition is what makes "compact" a property of the metric space (A,dA)(A,d_A) alone, so that a set compact in one ambient space is compact in every other one containing it isometrically.

The empty space is compact, since the empty subfamily of any family covers it; this is the reason the clause above is written with the two cases. The one-point space is compact too, and so is every space listed as {x0,,xn}\{x_0, \dots, x_n\}: given a cover, each xix_i lies in some member, and finitely many members chosen in this way already cover.

The finiteness convention, and how it is used both ways. "Finite" above is the listing form, matching the finite lists of Finite intersection property. It agrees with the definition of finiteness by equinumerosity with a natural number (Finite, countably infinite, countable, uncountable), and both directions of the agreement are available and are used below:

  • A nonempty finite set FF in the sense of Finite, countably infinite, countable, uncountable satisfies FmF \approx m for some m1m \ge 1, and a bijection mFm \to F is exactly a listing F={a0,,am1}F = \{a_0, \dots, a_{m-1}\}.
  • Conversely a set listed as A={a0,,an}A = \{a_0, \dots, a_n\}, that is the image of a function aa with domain σ(n)\sigma(n), is finite in the sense of Finite, countably infinite, countable, uncountable: the map sending xAx \in A to the least ini \le n with ai=xa_i = x is an injection of AA into σ(n)\sigma(n), so AA is equinumerous with a subset of N\mathbb{N} bounded above, and such a subset is finite (Every subset of an at most countable set is at most countable).

Neither direction uses a choice principle: the second selects nothing, taking a least index instead.

Remarks

Why open covers rather than closed ones. Nothing in the definition would break if U\mathcal{U} were allowed to consist of arbitrary sets, but the resulting notion would be uninteresting: every space is covered by its singletons, and only a finite space would survive. Openness of the members is what makes the condition a genuine restriction, and it is what A subset of a metric space is open in the subspace metric exactly when it is the trace of an open set of the ambient space, and it is compact as a metric space in its own right exactly when every family of open subsets of the ambient space covering it, indexed or not, has finitely many members covering it has to keep track of when the ambient space changes.

A warning about the word "cover". A family may cover AXA \subseteq X without being a family of subsets of AA: the members are open subsets of XX and their union merely contains AA. That is the ambient reading, and it is a different statement from "U\mathcal{U} is an open cover of the metric space (A,dA)(A,d_A)", whose members are open subsets of AA. Which of the two is meant is written out everywhere on this page.

Depends on

Used by

…and 29 more results.

Dependency tree · next 3 levels

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