OAI/Analysis/KadisonKastler/FiniteProjectionVectorCriterion.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finiteness from the faithful tracial vector identity on a corner

Only the norm identity for elements of the indicated corner is needed. This isolates the final projection argument from construction of the core's tracial vector.

  1. theorem OAI.KadisonKastler.operator_vector_norm_sq line 21
  2. theorem OAI.KadisonKastler.finiteProjectionIn_of_faithful_vector_norm line 27