OAI/Analysis/Pureness/Stabilization/Pullback.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CuntzTrace.Positive.map line 13
  2. def OAI.CuntzTrace.ExtendedTrace.pullback line 19
  3. theorem OAI.CuntzTrace.ExtendedTrace.pullback_apply line 45
  4. def OAI.CuntzTrace.ExtendedTrace.kernelWeight line 48
  5. theorem OAI.CuntzTrace.ExtendedTrace.kernelWeight_eq_zero line 50
  6. theorem OAI.CuntzTrace.ExtendedTrace.kernelWeight_lt_top line 53
  7. theorem OAI.CuntzTrace.ExtendedTrace.injective_of_surjective_pullback line 56