Density and cardinality

The faithful separable representation gives the carrier bound . Independently, the density obstruction gives for every norm-dense . Taking proves that the norm density is exactly and supplies the continuum-density counterexample.

Carrier cardinality, norm-density character and Hilbert-space dimension remain separate notions. The existence statement allows a possibly nonunital algebra and does not include a faithful separable representation as one of its quantified requirements. Its chosen witness happens to be the fixed unital algebra .

Exact Card references

Boundary Inputs

The displayed edges preserve dependency paths through omitted helpers. Levels count selected predecessors within this scope. Mathematical citations remain distinct from formal dependencies.

Exact source and provider boundary · Earlier 466-declaration Project view and PDF

Dependency-first reading route

Levels belong to this reading scope. Follow prerequisites or uses to focus the route.

Search declarations Route 2 declarations

Level 0

Level 0Focus target

Exact norm density of the fixed atomic algebra

MathlibAnnex.CStarAlgebra.CAR.hasDensityCharacter_atomicCounterexampleAlgebra

Combines a cardinality bound from a faithful representation on a separable Hilbert space with a lower bound for every norm-dense subset.

Immediate prerequisites in this Project
None in this scope

Used by in this Project
A Naimark counterexample of continuum norm density

Open Declaration Card Read exact source

Level 1

Level 1Focus target

A Naimark counterexample of continuum norm density

MathlibAnnex.CStarAlgebra.CAR.existsNaimarkCounterexampleOfDensity_continuum

Gives a C*-algebra of norm density whose nonzero irreducible representations form one unitary-equivalence class, without an identification with the compact operators.

Immediate prerequisites in this Project
Exact norm density of the fixed atomic algebra

Used by in this Project
None in this scope

Open Declaration Card Read exact source