Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-09-01
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.

The Cauchy-class operations of a normed-space completion are well defined

Statement

In the published Cauchy-sequence model of the metric completion of a normed space, if [xn] and [yn] denote equivalence classes of Cauchy sequences, then

[xn]+[yn]:=[xn+yn],λ[xn]:=[λxn],∥[xn]∥:=lim⁡n∥xn∥

are well defined.

Facts & Assumptions

Given: A normed space X; Cauchy sequences (xn), (xn′), (yn), (yn′) in X with [xn]=[xn′] and [yn]=[yn′] in the published completion model; and a scalar λ.

[L1]

The published metric completion is the quotient of the Cauchy sequences by the relation ρ((un),(vn))=0, where ρ((un),(vn))=lim⁡n∥un−vn∥ in the norm metric (Every metric space has a completion, constructed as the equivalence classes of its Cauchy sequences, A completion of a metric space: a complete metric space together with an isometric embedding onto a dense subspace).

[L2]

The norm satisfies the triangle inequality, absolute homogeneity, and the reverse triangle inequality (A norm on a real vector space, the induced metric, and the dictionary with the metric axioms, The reverse triangle inequality in a normed space).

[L3]

A real Cauchy sequence converges, limits are unique, and limits preserve non-strict inequalities and addition (Limits and Cauchy sequences of reals, A sequence has at most one limit, Limits preserve non-strict inequalities, Algebra of limits: sums, scalar multiples, products and quotients).

Proof

technique · direct
1.1

Termwise sums and scalar multiples of Cauchy sequences are again Cauchy: the triangle inequality gives ∥(xn+yn)−(xm+ym)∥≤∥xn−xm∥+∥yn−ym∥, and absolute homogeneity gives ∥λxn−λxm∥=∣λ∣ ∥xn−xm∥.

L2
1.2

Likewise ∥λxn−λxn′∥=∣λ∣ ∥xn−xn′∥ for every n, so [L1] and [L3] give ρ((λxn),(λxn′))=0. Hence scalar multiplication on classes is representative-independent.

L1L2L3
1.3

Because (xn) is Cauchy, the reverse triangle inequality in [L2] gives ∣∥xn∥−∥xm∥∣≤∥xn−xm∥; so the real sequence (∥xn∥) is Cauchy and therefore convergent by [L3].

L2L3
2.1

If [xn]=[xn′] and [yn]=[yn′], then ∥(xn+yn)−(xn′+yn′)∥≤∥xn−xn′∥+∥yn−yn′∥ for every n; passing to limits and using [L1] and [L3] gives ρ((xn+yn),(xn′+yn′))=0. So addition on classes is representative-independent.

step 1.1L1L2L3
3.1

If [xn]=[xn′], then ∣∥xn∥−∥xn′∥∣≤∥xn−xn′∥ for every n; the right-hand side tends to 0 by [L1], so the two real norm sequences have the same limit by [L3]. Thus ∥[xn]∥:=lim⁡n∥xn∥ is well defined.

step 1.3L1L2L3∎

Depends on

Used by

Dependency tree · two levels

51 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