OAI/Analysis/KadisonKastler/CountableProjectionFamilies.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Countable projection families from separating vectors

The spatial derivation argument needs countable decomposability of the algebra, rather than separability of the ambient Hilbert space. A countable family of separating vectors supplies exactly this property.

  1. def OAI.KadisonKastler.HasCountableProjectionFamilies line 26
  2. theorem OAI.KadisonKastler.projection_norm_apply_sq line 31
  3. theorem OAI.KadisonKastler.countable_projection_vector_support line 38
  4. theorem OAI.KadisonKastler.countableProjectionFamilies_of_separating_vectors line 75