OAI/Analysis/Pureness/Completion/SharedMatrixBridge.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CuntzPureness.shared_matrixSuccessor_eq_corner line 10
  2. lemma OAI.CuntzPureness.shared_matrixInclusion_eq_corner line 19
  3. lemma OAI.CuntzPureness.completedMatrixInclude_shared_compatible line 29
  4. def OAI.CuntzPureness.sharedMatrixToCompletion line 33
  5. lemma OAI.CuntzPureness.sharedMatrixToCompletion_stage line 36
  6. lemma OAI.CuntzPureness.sharedMatrixToCompletion_continuous line 40
  7. lemma OAI.CuntzPureness.sharedMatrixToCompletion_norm line 47
  8. lemma OAI.CuntzPureness.sharedMatrixToCompletion_isometry line 57
  9. lemma OAI.CuntzPureness.sharedMatrixToCompletion_surjective line 60
  10. def OAI.CuntzPureness.sharedMatrixEquiv line 73
  11. theorem OAI.CuntzPureness.sharedMatrixEquiv_stage line 77