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))
Definition
Let be a normed space and let be a linear subspace. For a coset , define
Equivalently, this is the distance from to inside the ambient normed space:
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.
Remarks
- The word seminorm is deliberate: definiteness is the next theorem, and it requires closedness of .
- No nearest point is assumed to exist. The definition uses an infimum only.
Depends on
Used by
- For real continuous functions modulo constants, the quotient norm is half the oscillation Example
- The quotient by the kernel is isometric to the range with its induced quotient norm Example
- The quotient seminorm is independent of the chosen coset representative Lemma
- The quotient seminorm satisfies the triangle inequality Lemma
- A bounded operator that vanishes on a subspace factors uniquely through the normed quotient Theorem
- A quotient of a Banach space by a closed subspace is Banach Theorem
- The quotient map sends every open ball onto a set containing the corresponding quotient ball Theorem
- The quotient seminorm is a norm exactly when the subspace is closed Theorem
Dependency tree · two levels
17 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
- Gerald Teschl, Topics in Real and Functional Analysis (standard reference, not scraped)
- Theo Buhler and Dietmar A. Salamon, Functional Analysis (standard reference, not scraped)