Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: 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.

Coordinate projections and inclusions on a finite product Banach space

Example

Let X and Y be Banach spaces over the same scalar field and equip X×Y with the maximum product norm

∥(x,y)∥max⁡:=max⁡{∥x∥,∥y∥}.

Then the coordinate projections

πX(x,y)=x,πY(x,y)=y,

and the coordinate inclusions

ιX(x)=(x,0),ιY(y)=(0,y)

are bounded linear operators. Moreover,

∥πX∥=∥ιX∥={1,X≠{0},0,X={0},∥πY∥=∥ιY∥={1,Y≠{0},0,Y={0}.

Facts & Assumptions

Given: Banach spaces X and Y over the same scalar field, their product X×Y with the maximum norm, and vectors x∈X, y∈Y.

[L1]

The maximum product norm is one of the standard product norms (The standard product norms on a finite product of normed spaces).

[L2]

A finite product of Banach spaces is Banach, and bounded linear operators are the members of B(⋅,⋅) (Finite products of Banach spaces are Banach, A bounded linear operator between normed spaces, The spaces (\mathcal B(X,Y)) and (\mathcal B(X)) of bounded linear operators).

[L3]

The operator norm is the unit-ball supremum and therefore records the least global bound of a bounded linear operator (The operator norm as the least bound and as the unit-sphere or unit-ball supremum).

Verification

technique · direct
1.1L1L2L3

By [L1], ∥(x,y)∥max⁡≥∥x∥ and ∥(x,y)∥max⁡≥∥y∥, so ∥πX(x,y)∥≤∥(x,y)∥max⁡ and ∥πY(x,y)∥≤∥(x,y)∥max⁡. Thus both projections are bounded with operator norm at most 1 by [L2] and [L3].

2.1step 1.1L1L3choose

For x∈X and y∈Y, [L1] gives ∥ιX(x)∥max⁡=∥(x,0)∥max⁡=∥x∥ and ∥ιY(y)∥max⁡=∥(0,y)∥max⁡=∥y∥. So ∥ιX∥≤1 and ∥ιY∥≤1, with equality whenever the relevant domain is nonzero. If X≠{0}, choose u∈X with ∥u∥=1. Then ∥ιX(u)∥max⁡=1, and also ∥πX(u,0)∥=1=∥(u,0)∥max⁡, so ∥ιX∥=∥πX∥=1. If X={0}, then both ιX and πX are the zero operator, so both norms are 0. The same argument with Y gives the corresponding statements for ιY and πY.

3.1step 1.1step 2.1L2∎

Therefore πX∈B(X×Y,X), πY∈B(X×Y,Y), ιX∈B(X,X×Y), and ιY∈B(Y,X×Y), with the norms stated above.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

14 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