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 bounded operator that vanishes on a subspace factors uniquely through the normed quotient

Statement

Let $X$ and $Y$ be normed spaces over the same scalar field, let $M \leq X$ be a closed linear subspace, let $q : X \to X / M$ be the quotient map, and let $T : X \to Y$ be a bounded linear operator with $M \subseteq \ker T$ . Then there is a unique bounded linear operator $\overline{T} : X / M \to Y$ such that

$\overline{T} \circ q = T,$

and moreover $∥ \overline{T} ∥ = ∥ T ∥$ .

Facts & Assumptions

Given: A closed linear subspace $M \leq X$ , the quotient map $q : X \to X / M$ , and a bounded linear operator $T : X \to Y$ with $M \subseteq \ker T$ .

[L1]

The algebraic quotient universal property gives a unique linear map $\overline{T} : X / M \to Y$ with $\overline{T} (q x) = T x$ (Universal property of the quotient vector space).

[L2]

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

[L3]

A bounded operator has a concrete bound, and $q (x) = x + M$ (A bounded linear operator between normed spaces, The quotient vector space (X/M), its cosets, and the quotient map (q:X\to X/M)).

[L4]

The quotient map sends the open unit ball of $X$ onto a set containing the open unit ball of $X / M$ (The quotient map sends every open ball onto a set containing the corresponding quotient ball).

Proof

technique · direct

1.1

By [L1], there is a unique linear map $\overline{T} : X / M \to Y$ with $\overline{T} (q x) = T x$ for every $x \in X$ . This proves representative independence before any norm estimate.

2.1

Let $ξ = x + M$ and let $m \in M$ . Since $T m = 0$ , $\overline{T} (ξ) = T x = T (x + m)$ . If $C$ is a bound for $T$ from [L3], then $∥ \overline{T} (ξ) ∥ \leq C ∥ x + m ∥$ for every $m \in M$ . Taking the infimum over $m$ and using [L2] gives $∥ \overline{T} (ξ) ∥ \leq C ∥ ξ ∥_{X / M}$ . Hence $\overline{T}$ is bounded and $∥ \overline{T} ∥ \leq ∥ T ∥$ .

step 1.1L2L3

3.1

For every $x \in X$ , $∥ q (x) ∥_{X / M} \leq ∥ x ∥$ because the infimum in [L2] can be evaluated at $m = 0$ . Therefore $∥ T x ∥ = ∥ \overline{T} (q x) ∥ \leq ∥ \overline{T} ∥ ∥ x ∥$ by step 2.1. Taking the supremum over $∥ x ∥ \leq 1$ gives $∥ T ∥ \leq ∥ \overline{T} ∥$ .

step 2.1L2L3

4.1

Step 2.1 gave $∥ \overline{T} ∥ \leq ∥ T ∥$ , and step 3.1 gave the reverse inequality, so $∥ \overline{T} ∥ = ∥ T ∥$ . The unit-ball content of [L4] is the same geometric reason that no larger quotient bound is needed.

step 2.1step 3.1L4

5.1

The linear map in step 1.1 is therefore the unique bounded factor of $T$ through the normed quotient, and it has the same operator norm.

step 1.1step 4.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

12 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

Theo Buhler and Dietmar A. Salamon, Functional Analysis (standard reference, not scraped)
Gerald Teschl, Topics in Real and Functional Analysis (standard reference, not scraped)