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.

Cauchy sequence in a metric space

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) and let (xk) be a sequence in X, that is a function N→X written xk:=x(k) (Convergence of a sequence in a metric space: xk→x iff d(xk,x)→0 in R, Sequences of reals: bounded, eventually, frequently, tails, subsequences). As everywhere in this library N contains 0, so a sequence is indexed from 0.

(xk) is a Cauchy sequence in (X,d) if for every rational ε>0 there is K∈N such that

d(xm,xn)<εfor all m,n≥K.

Rational and real ε agree here. The test is written with a rational ε to match Limits and Cauchy sequences of reals and Convergence of a sequence in a metric space: xk→x iff d(xk,x)→0 in R, and nothing is lost by using a real one: 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 Cauchyness by producing an index for every real ε>0, and may use a Cauchy hypothesis at a real ε by first passing to a rational below it. Both moves are used on this page and are always cited.

The condition is exactly d(xm,xn)→0 as m and n grow independently. The distances d(xm,xn) are nonnegative reals (Nonnegativity of a metric is a consequence of the other axioms, not an axiom), and the displayed condition asks them to be uniformly small on a tail of the doubly indexed family. It is not the same as d(xk+1,xk)→0, which is a strictly weaker condition and is a standing source of error. The partial sums Hn of the harmonic series separate the two: consecutive ones differ by 1/(n+1), which tends to 0, while the sequence is unbounded, and an unbounded sequence of reals is not Cauchy (Every Cauchy sequence in a metric space is bounded).

Consistency with the real line. For X=R with the usual metric d(x,y)=∣x−y∣ (The absolute value makes R a metric space: d(x,y)=∣x−y∣ is a metric, its open balls are the intervals (x−r,x+r), and it is unbounded) the condition above reads ∣xm−xn∣<ε for m,n≥K, which is verbatim the definition of a Cauchy sequence of reals (Limits and Cauchy sequences of reals). So the notion introduced here restricts on R to the one already in use, and no ambiguity is created.

Remarks

Depends on

Used by

…and 2 more results.

Dependency tree · two levels

39 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