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

Convergence of a sequence in a metric space: xk→x iff d(xk,x)→0 in R

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).

A sequence in X is a function x:N→X, written (xk) with xk:=x(k). As everywhere in this library, N contains 0 (The natural numbers N (von Neumann)) and a sequence is indexed from 0 (Sequences of reals: bounded, eventually, frequently, tails, subsequences); an index range copied from a text that starts at 1 must be shifted before it is used here.

Let (xk) be a sequence in X and p∈X. The function k↦d(xk,p) is a sequence of reals (Sequences of reals: bounded, eventually, frequently, tails, subsequences), and it is nonnegative (Nonnegativity of a metric is a consequence of the other axioms, not an axiom), so ∣d(xk,p)∣=d(xk,p) (Absolute value in an ordered field). Define

xk⟶p in (X,d):⟺d(xk,p)⟶0 in R,

the convergence on the right being that of Limits and Cauchy sequences of reals. Unwound, this says: for every rational ε>0 there is K∈N with d(xk,p)<ε for every k≥K. We then call p a limit of (xk), and say (xk) converges in (X,d) if it has a limit.

Rational and real ε agree here, as they do on the real line. Limits and Cauchy sequences of reals tests convergence against rational ε only, and its own remark, restated for sequences in Sequences of reals: bounded, eventually, frequently, tails, subsequences, records that nothing is lost: below any real η>0 lies a positive rational (The rationals embed densely in the reals), and the index belonging to that rational serves for η. So a proof may establish convergence by producing an index for every real ε>0, and may use a convergence hypothesis at a real ε by first passing to a rational below it. Both moves are used on this page and are always cited.

Subsequences and subsequential limits. A subsequence of (xk) is the composite x∘n for a strictly increasing n:N→N, written (xnj), exactly as for sequences of reals (Sequences of reals: bounded, eventually, frequently, tails, subsequences); and p is a subsequential limit of (xk) in (X,d) when some subsequence converges to p, which is the metric-space form of Subsequential limit of a real sequence, and the subsequential limit set.

Remarks

Depends on

Used by

…and 62 more results.

Dependency tree · two levels

27 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