OAI/Analysis/Commutator/BiprodLinkColumn.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Kadison.BiprodLinkColumn.Intertwiner line 27
  2. lemma OAI.Kadison.BiprodLinkColumn.inl_norm_le line 30
  3. lemma OAI.Kadison.BiprodLinkColumn.inr_norm_le line 34
  4. def OAI.Kadison.BiprodLinkColumn.component line 37
  5. lemma OAI.Kadison.BiprodLinkColumn.component_adjoint line 40
  6. lemma OAI.Kadison.BiprodLinkColumn.source_adjoint line 45
  7. lemma OAI.Kadison.BiprodLinkColumn.inr_component line 54
  8. lemma OAI.Kadison.BiprodLinkColumn.component_square line 59
  9. def OAI.Kadison.BiprodLinkColumn.finiteColumn line 68
  10. def OAI.Kadison.BiprodLinkColumn.compression line 71
  11. lemma OAI.Kadison.BiprodLinkColumn.column_square line 74
  12. lemma OAI.Kadison.BiprodLinkColumn.compression_norm_le line 85
  13. lemma OAI.Kadison.BiprodLinkColumn.column_norm_le line 97
  14. lemma OAI.Kadison.BiprodLinkColumn.compression_tendsto line 102
  15. lemma OAI.Kadison.BiprodLinkColumn.component_intertwines line 115