OAI/Analysis/Commutator/MatrixCornerExtension.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Kadison.MatrixCornerExtension.mapped_col line 35
  2. lemma OAI.Kadison.MatrixCornerExtension.mapped_init line 40
  3. lemma OAI.Kadison.MatrixCornerExtension.mapped_total line 45
  4. def OAI.Kadison.MatrixCornerExtension.columns line 48
  5. lemma OAI.Kadison.MatrixCornerExtension.columns_total line 52
  6. lemma OAI.Kadison.MatrixCornerExtension.columns_project line 58
  7. lemma OAI.Kadison.MatrixCornerExtension.final_support line 66
  8. def OAI.Kadison.MatrixCornerExtension.entry line 69
  9. lemma OAI.Kadison.MatrixCornerExtension.columns_block line 74
  10. def OAI.Kadison.MatrixCornerExtension.extend line 83
  11. lemma OAI.Kadison.MatrixCornerExtension.extend_norm_le line 87
  12. lemma OAI.Kadison.MatrixCornerExtension.extend_intertwines line 91
  13. def OAI.Kadison.MatrixCornerExtension.cornerMap line 104
  14. lemma OAI.Kadison.MatrixCornerExtension.norm_sub_extend_le line 110