OAI/Analysis/KadisonSimilarity/Representation/SpectralBaseTopology.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The spectrum of a norm-separable commutative C-star algebra is a compact metrizable base for its vector spectral measures.

  1. theorem OAI.KadisonSimilarity.characterSpace_metrizable line 14
  2. theorem OAI.KadisonSimilarity.characterSpace_secondCountable line 19