OAI/Analysis/Pureness/States/RegularizedStateQuasitrace.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CuntzPureness.regularizedState_dimension_finite line 11
  2. lemma OAI.CuntzPureness.regularizedState_dimension_lsc line 19
  3. def OAI.CuntzPureness.regularizedStateTwoQuasitrace line 29
  4. theorem OAI.CuntzPureness.regularizedStateTwoQuasitrace_unit_pos line 35
  5. theorem OAI.CuntzPureness.regularizedStateQuasitrace_root_rank line 44