Complete metric space: proving every finite metric space complete by the least positive distance, contrasted with (0,1]

Goal and scope

Prove that every finite metric space (X,d) with at least one point is complete (immediate for a single point; with at least two points, the least positive distance δ forces every Cauchy sequence to be ultimately constant). On X0={0,1,3} with d(x,y)=|x−y|, compute δ=1, give an ultimately constant certificate and an explicit non-Cauchy sequence; finally prove that the subspace Y=(0,1] is not complete: x_n=1/n is Cauchy in Y but has no limit in Y.

Stays inside the MKO: the finite certificate uses a complete finite metric table with at least one point; the least-positive-distance argument uses at least two (assumption a1); sequence exercises accept only an explicit ultimately constant certificate or an explicit non-Cauchy counterexample, and a finite prefix is not a completeness proof (assumption a2). The contrast with (0,1] uses reciprocal-sequence bounds as a complete certificate. Completions in general and Banach spaces are not treated; the canonical MKO and its English edition are not changed.

Givens and symbols

• metric_def
• order_basics
• abs_rules
• archimedean
• min_finite

• G1 — (X,d) is a finite metric space, X has at least one point, and the metric table is complete.
• G2 — Example: X0={0,1,3} with d(x,y)=|x−y| (the usual distance of ℝ restricted to X0).
• G3 — Contrast: Y=(0,1]={t∈ℝ : 0<t≤1} with d(s,t)=|s−t|; the sequence x_n=1/n (n≥1).

• (X,d) — finite metric space
• (x_n) — a sequence in X, n=1, 2, 3 and so on
• \delta — least positive distance min{d(x,y): x≠y}
• N — index threshold in the Cauchy or convergence definition
• X_0 — the example {0,1,3} with d(x,y)=|x−y|
• Y — the subspace (0,1] with d(s,t)=|s−t|

Rules and sources

• metric_def · prerequisite — Metric: d:X×X→ℝ with d(x,y)≥0 and d(x,y)=0 ⇔ x=y; d(x,y)=d(y,x); triangle inequality d(x,z)≤d(x,y)+d(y,z).
• order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
• abs_rules · prerequisite — Absolute value (reals): |u|=u if u≥0 and |u|=−u if u<0; |u|≥0; |uv|=|u||v|; triangle inequality |u+v|≤|u|+|v|; |u|<r ⇔ −r<u<r.
• archimedean · prerequisite — Archimedean property: for every real x there is a natural number n>x; hence for every ε>0 there is n with 1/n<ε.
• def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
• case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility.
• forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain.
• def_intro · prerequisite — Introducing a definition: a statement, expression or object may be given a name, after which the name and what it stands for are interchangeable.
• contrapositive · prerequisite — Contrapositive: P⇒Q is equivalent to ¬Q⇒¬P. The converse Q⇒P is in general not equivalent to P⇒Q.
• forall_elim · prerequisite — ∀-elimination (instantiation): if ∀x∈D, P(x) holds and a∈D, then P(a) holds.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
• contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds.
• mko_complete_def · cited — Independent append-only source erratum (owner-adopted in this local revision; not merged or published): a metric space (X,d) is complete if every Cauchy sequence in X converges to a point of X. For a finite space with at least two points, the finite nonempty positive-distance set has a minimum forcing Cauchy tails to be ultimately constant. In the singleton case every sequence is already constant, with no minimum positive distance required or defined. Sampled sequences do not prove general completeness. The original citation and canonical MKO are preserved. · mko-complete-metric-space
• mko_cauchy_def · cited — A sequence (x_n) is Cauchy if for every epsilon>0 there exists N such that all m,n≥N satisfy d(x_m,x_n)<epsilon. The definition does not first assume that a limit exists or belongs to the space. · mko-cauchy-sequence
• mko_conv_def · cited — A sequence x_n in a metric space converges to x if, for every epsilon>0, there exists N such that all n≥N satisfy d(x_n,x)<epsilon. Passing a sampled finite tail is insufficient for general convergence; an explicitly ultimately constant infinite sequence can instead provide a complete witness. · mko-metric-convergence
• min_finite · prerequisite — A nonempty finite set of reals has a least element, and that least element belongs to the set.
• L_small_dist · lemma — In a finite metric space with at least two points let δ=min{d(x,y) : x≠y}. Then δ>0, and d(x,y)<δ implies x=y.
• L_limit_unique · lemma — In a metric space, if x_n→L and x_n→L′, then L=L′.

Main derivation

(X,d)\ \text{complete}

\forall (x_n)\subseteq X\ \text{Cauchy}\ \exists L\in X:\ x_n\to L

|X|\ge 1

|X|=1\ \lor\ |X|\ge 2

X=\{p\}

x_n=p\ \forall n,\ d(x_n,p)=0<\varepsilon\ \Rightarrow\ x_n\to p\in X

D=\{d(x,y): x,y\in X,\ x\neq y\}

\delta=\min D

\delta=\min D

\delta>0,\ d(x,y)<\delta\Rightarrow x=y

(x_n)\ \text{Cauchy in}\ X,\ \varepsilon=\delta>0

\exists N\ \forall m,n\ge N:\ d(x_m,x_n)<\delta

d(x_N,x_n)<\delta\ \ (n\ge N)

x_n=x_N\ \ \text{for all}\ n\ge N

L=x_N\in X,\ \varepsilon>0

\forall n\ge N:\ d(x_n,L)=0<\varepsilon\ \Rightarrow\ x_n\to L

(x_n)\ \text{an arbitrary Cauchy sequence in}\ X

\text{every Cauchy sequence in}\ X\ \text{converges in}\ X\ \ (|X|\ge 2)

|X|=1\ \lor\ |X|\ge 2

(X,d)\ \text{complete}

d(0,1),\ d(0,3),\ d(1,3)

1,\ 3,\ 2;\ \delta=\min(1,3,2)=1

x_1=0,\ x_2=3,\ x_n=1\ (n\ge 3)

(x_n)\ \text{Cauchy with}\ N=3,\ x_n\to 1\in X_0

x_n=0\ (n\ \text{odd}),\ x_n=1\ (n\ \text{even})

\text{not Cauchy: for}\ \varepsilon=\tfrac12,\ d(x_N,x_{N+1})=1\ge\tfrac12\ \forall N

x_n=\tfrac1n\in Y,\ \varepsilon>0

\exists N:\ \forall m,n\ge N,\ \left|\tfrac1m-\tfrac1n\right|<\tfrac1N<\varepsilon

\left|\tfrac1n-0\right|=\tfrac1n

x_n\to 0\ \text{in}\ \mathbb{R}

x_n\to L,\ x_n\to L'

L=L'

x_n\to L\ \text{in}\ Y\ \text{for some}\ L\in Y

L=0\notin Y\ \Rightarrow\ Y\ \text{not complete}

Substeps and lemmas

\delta\in D

\delta>0

x\neq y\Rightarrow d(x,y)\in D\Rightarrow d(x,y)\ge\delta

d(x,y)<\delta\Rightarrow x=y

d(x_n,L)<\varepsilon\ (n\ge N_1),\ d(x_n,L')<\varepsilon\ (n\ge N_2)

d(L,L')<2\varepsilon\ \ \text{for every}\ \varepsilon>0

d(L,L')<2\varepsilon\ \forall\varepsilon>0

L=L'

Reverse audits

• S17 · sufficient_goal_reduction · S14, S15, S16, contradiction — Goal G: Y is not complete. Sufficient condition H: some Cauchy sequence in Y does not converge in Y; H⇒G by the definition of completeness (one counterexample refutes a universal). H is proved forwards in S14 to S16.
• S16.2 · premise_audit · S16.1, metric_def, contradiction — It uses separation: distinct points are at positive distance; this sub-step does not use L_limit_unique.
• S16.1 · premise_audit · metric_def, mko_conv_def — It needs one n beyond both thresholds; this sub-step does not use L_limit_unique.
• S16 · premise_audit · metric_def, L_limit_unique — It needs only the metric axioms and holds in every metric space.
• S15 · premise_audit · archimedean, mko_conv_def — This is convergence in the ambient space ℝ; on its own it says nothing about whether Y is complete.
• S14 · premise_audit · archimedean, mko_cauchy_def, abs_rules — It uses 'the difference of two positive numbers is less than the larger' and the Archimedean property; this is a reciprocal-bound certificate for every ε, and N6 is only a check on a finite range.
• S13 · premise_audit · mko_cauchy_def, quantifier_negation — Negating '∀ε ∃N ∀m,n' needs one ε and, for each N, one failing pair; this is an explicit non-Cauchy counterexample.
• S12 · premise_audit · mko_cauchy_def, mko_conv_def — The certificate rests on the explicit declaration that all later terms equal 1, not on a listed finite prefix.
• S11 · premise_audit · G2, numeric_evaluation — All three pairs of the complete distance table are computed; omitting one could give a wrong δ.
• S10 · sufficient_goal_reduction · S01, S02, S03, S09, case_analysis — Goal G: X is complete. Sufficient condition H: in both cases every Cauchy sequence converges in X; H⇒G by the definition and proof by cases. H is proved forwards in S03 and S09.
• S09 · premise_audit · S06, S07, S08, forall_intro — Generalization requires the sequence to be arbitrary; no particular sequence was used.
• S08 · premise_audit · S07, metric_def, mko_conv_def — One N serves every ε because the tail distances are exactly 0; L∈X because it is a term of the sequence.
• S07 · premise_audit · S05, S06 — It needs m=N to lie in the range m≥N; the conclusion concerns only terms with n≥N, and earlier terms may be anything.
• S06 · premise_audit · mko_cauchy_def, S05, forall_elim — ∀-elimination needs δ in the range of ε, that is δ>0; no converse is claimed.
• S05.2 · inverse_equivalence · contrapositive — A statement and its contrapositive are equivalent, so the step is two-way. This sub-step does not use L_small_dist.
• S05.1 · premise_audit · metric_def, min_finite — It uses that the minimum is attained; a mere infimum that is not attained could be 0. This sub-step does not use L_small_dist.
• S05 · premise_audit · S04, L_small_dist — The lemma needs a finite space with at least two points, which S04 provides.
• S04 · premise_audit · S02, min_finite — It needs both finiteness and nonemptiness; in an infinite space such a minimum may fail to exist (distances in Y can be arbitrarily small).
• S03 · premise_audit · S02, metric_def, mko_conv_def — It uses only d(p,p)=0; this case does not need the least positive distance.
• S02 · premise_audit · G1, case_analysis — The two cases cover every finite set with at least one point and do not overlap.
• S01 · premise_audit · mko_complete_def, mko_cauchy_def, mko_conv_def — This step only unfolds the three definitions and derives no new fact.

Error controls and negative controls

Completeness is a property of the space, not of a few tested sequences

The common mistake named by the MKO is to declare completeness after a few tested sequences converge. In Y=(0,1], the constant sequence 1/2 and the sequence 1/2+1/(2n) both converge in Y, but 1/n does not (S17). Completeness must hold for every Cauchy sequence; the finite-space proof (S06 to S09) works with an arbitrary Cauchy sequence.

A limit in the ambient space does not count

1/n converges to 0 in ℝ, but 0∉(0,1], so (0,1] is not complete. Conversely, X0={0,1,3} is complete by the finite argument of S10, not because ℝ is complete. Completeness requires the limit to belong to the space itself.

A finite prefix is not a certificate

Listing the first 1000 terms of a sequence as 1 does not show that later terms are 1. The MKO accepts only an ultimately constant certificate that explicitly declares every later term equal to the tail value (S12), or an explicit non-Cauchy counterexample (S13). Likewise δ must come from every pair of the complete distance table (S11).

• (0,1] is complete because 1/n has the limit 0 in ℝ → reject — 0∉(0,1] and limits are unique, so 1/n has no limit in (0,1].
• The alternating sequence 0, 1, 0, 1 and so on in X0 does not converge, so X0 is not complete → reject — It is not Cauchy (S13); completeness only requires Cauchy sequences to converge.
• Five Cauchy sequences in (0,1] were tested and all converged in (0,1], so (0,1] is complete → reject — 1/n is a Cauchy sequence in (0,1] with no limit in (0,1].
• In a finite metric space a Cauchy sequence is constant from its first term → reject — The sequence 0, 3, 1, 1, 1 and so on is Cauchy in X0 but its first two terms differ; only ultimately constant is guaranteed.

Result and limitations

Every finite metric space with at least one point is complete: with one point every sequence is constant; with at least two, the least positive distance δ>0 used as ε in the Cauchy definition forces the sequence to equal x_N from some N on, so it converges to x_N∈X. For X0={0,1,3}, δ=1; the sequence 0, 3, 1, 1, 1 and so on has the ultimately constant certificate N=3; the alternating 0, 1 sequence is not Cauchy. The subspace (0,1] is not complete: 1/n is Cauchy, but its only possible limit 0 is not in (0,1].

• N6 checks |1/m−1/n|<1/min(m,n) only on the finite range 1≤m,n≤30; the proof for all m, n is the argument of S14.
• min_finite is a premise of this guide; that 1/2+1/(2n) converges in Y is explanatory in the error controls and not a numbered step.

Verification and source binding

7 declared checks for this guide; only the listed expressions are covered.

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: f777d86bce746681448ac94bc6f723103abd39b7d9520aa52006b6c641835c8d
• original source SHA-256: 1db5dbc4b9d2cc946ce1390b35ee86de434aefd9ce839d023e2612e22357f1e8
• Lean: NOT_RUN · independent AI: NOT_MEASURED

Same-source full JSON (formulas, ASTs, controls and revision log)