Alphabeta Math
TheoremStatement: 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.

Finite products of Banach spaces are Banach

Statement

Let n≥1, and let E0,…,En−1 be Banach spaces. Then their finite product ∏k<nEk is a Banach space for each of the standard product norms ∥⋅∥max⁡, ∥⋅∥2, and ∥⋅∥1.

Facts & Assumptions

Given: A natural number n≥1, Banach spaces E0,…,En−1, and a Cauchy sequence x(m)=(x0(m),…,xn−1(m)) in the product for the maximum norm.

[L1]

A Banach space is complete for its norm metric (Banach space).

[L2]

The maximum, Euclidean, and sum product norms are defined on the finite product (The standard product norms on a finite product of normed spaces).

[L3]

These three product norms satisfy ∥x∥max⁡≤∥x∥2≤∥x∥1≤n∥x∥max⁡ (The standard finite product norms are equivalent).

Proof

technique · direct
1.1L2given

If x(m) is Cauchy for ∥⋅∥max⁡, then each coordinate sequence (xk(m))m is Cauchy in Ek, because ∥xk(m)−xk(ℓ)∥≤∥x(m)−x(ℓ)∥max⁡ for every k<n.

2.1step 1.1L1construct

Since each Ek is Banach, [L1] gives a point xk∈Ek with xk(m)→xk. Put x:=(x0,…,xn−1).

3.1step 2.1givenchoose

Given ε>0, choose M0 so that ∥x(m)−x(ℓ)∥max⁡<ε/2 for m,ℓ≥M0, and for each k<n choose Mk so that ∥xk(m)−xk∥<ε/2 for m≥Mk. For M:=max⁡{M0,M1,…,Mn−1} and m≥M, taking ℓ→∞ in a fixed coordinate gives ∥xk(m)−xk∥≤ε/2 for every k<n, hence ∥x(m)−x∥max⁡≤ε/2<ε.

4.1step 3.1L1

Thus the product is complete for the maximum norm, hence Banach for that norm by [L1].

5.1step 4.1L3∎

The inequalities in [L3] show that a sequence is Cauchy or convergent for one standard product norm exactly when it is so for the others. Therefore completeness for ∥⋅∥max⁡ is equivalent to completeness for ∥⋅∥2 and for ∥⋅∥1, so the product is Banach for all three norms.

Depends on

Used by

Dependency tree · two levels

9 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