OAI/Analysis/BoundedHochschild/CentralIsometries.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Central cuts and extensions of partial isometries.

  1. lemma OAI.HochschildCentralComparison.central_mul_pair line 22
  2. lemma OAI.HochschildCentralComparison.central_mul_sandwich line 30
  3. lemma OAI.HochschildCentralComparison.centralProjection_mul line 34
  4. lemma OAI.HochschildCentralComparison.centralProjection_one_sub line 38
  5. def OAI.HochschildCentralComparison.PartialIso.centralCut line 43
  6. lemma OAI.HochschildCentralComparison.PartialIso.centralCut_coe line 51
  7. lemma OAI.HochschildCentralComparison.PartialIso.centralCut_initial line 55
  8. lemma OAI.HochschildCentralComparison.PartialIso.centralCut_final line 61
  9. lemma OAI.HochschildCentralComparison.PartialIso.centralCut_initial_le line 66
  10. lemma OAI.HochschildCentralComparison.PartialIso.centralCut_final_le line 71
  11. theorem OAI.HochschildCentralComparison.PartialIso.unitary_extension line 82