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.

A quotient of a Banach space by a closed subspace is Banach

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice (ACω)).

Let X be a Banach space and let M≤X be a closed linear subspace. Then X/M is Banach for the quotient norm.

Facts & Assumptions

Given: The Axiom of Countable Choice, a Banach space X, a closed linear subspace M≤X, and a Cauchy sequence (ξn) in X/M.

[L0]

Countable Choice is assumed (The Axiom of Countable Choice (ACω)).

[L1]

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

[L2]

The quotient norm is ∥x+M∥X/M=inf⁡m∈M∥x+m∥ (The quotient seminorm (|x+M|{X/M}=\inf{m\in M}|x+m|=\operatorname{dist}(x,M))).

[L3]

Because M is closed, the quotient seminorm is a norm on X/M (The quotient seminorm is a norm exactly when the subspace is closed).

[L4]

In a Banach space, every absolutely convergent series converges (Series criterion for Banach spaces).

Proof

technique · direct
1.1givenchoose

Since (ξn) is Cauchy in X/M, choose a strictly increasing sequence (nk) such that ∥ξnk+1−ξnk∥X/M<2−k for every k≥0.

2.1L0step 1.1L2choose

For each k, choose uk∈X representing ξnk+1−ξnk and satisfying ∥uk∥<2−k+2−2k. This is possible by [L0], [L2], and step 1.1.

3.1step 2.1L1L4

The series ∑kuk is absolutely convergent because ∑k(2−k+2−2k) converges. Since X is Banach, [L4] gives a vector u∈X with ∑kuk=u.

4.1step 3.1L2

Let sj:=∑k=0j−1uk. Because each uk represents ξnk+1−ξnk, the coset q(sj) equals ξnj−ξn0. Therefore ξnj=ξn0+q(sj). Since sj→u in X, the tails satisfy ∥u−sj∥→0, and [L2] gives ∥q(u)−q(sj)∥X/M≤∥u−sj∥. Hence ξnj→η:=ξn0+q(u) in X/M.

5.1

The whole sequence (ξn) converges to η. Given ε>0, choose J so that ∥ξn−ξm∥X/M<ε/2 for all m,n≥J, and also choose k with nk≥J and ∥ξnk−η∥X/M<ε/2 from step 4.1. Then for every n≥J,

∥ξn−η∥X/M≤∥ξn−ξnk∥X/M+∥ξnk−η∥X/M<ε.

So (ξn) converges in X/M. [step 4.1, given, choose]

6.1step 5.1L1L3∎

Every Cauchy sequence in X/M converges, so X/M is Banach by [L1].

Depends on

Used by

Dependency tree · two levels

20 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