DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 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 quotient seminorm (|x+M|{X/M}=\inf{m\in M}|x+m|=\operatorname{dist}(x,M))

Let $X$ be a normed space and let $M \leq X$ be a linear subspace. For a coset $x + M \in X / M$ , define

$∥ x + M ∥_{X / M} : = \inf_{m \in M} ∥ x + m ∥ .$

Equivalently, this is the distance from $x$ to $M$ inside the ambient normed space:

$∥ x + M ∥_{X / M} = dist (x, M) .$

The formula is representative-independent by The quotient seminorm is independent of the chosen coset representative ↗, so it is a well-defined seminorm on the quotient vector space.

The word seminorm is deliberate: definiteness is the next theorem, and it requires closedness of $M$ .
No nearest point is assumed to exist. The definition uses an infimum only.

Depends on