OAI/Analysis/CStarAlgebra/PureInfiniteness/OrthogonalSlots.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MainGap.cut_map line 23
  2. def OAI.MainGap.entry line 29
  3. lemma OAI.MainGap.entry_apply line 32
  4. lemma OAI.MainGap.entry_mul line 35
  5. lemma OAI.MainGap.entry_mul_of_ne line 39
  6. lemma OAI.MainGap.star_entry line 43
  7. lemma OAI.MainGap.entry_add line 51
  8. lemma OAI.MainGap.entry_smul line 54
  9. lemma OAI.MainGap.entry_zero line 57
  10. def OAI.MainGap.cornerHom line 60
  11. lemma OAI.MainGap.diagonalCorner_mul line 68
  12. lemma OAI.MainGap.star_diagonalCorner line 72
  13. def OAI.MainGap.diagonalHom line 80
  14. lemma OAI.MainGap.corner_cut line 88
  15. lemma OAI.MainGap.diagonal_cut line 92
  16. lemma OAI.MainGap.continuous_entry line 96
  17. lemma OAI.MainGap.entry_mem_diagonalHer line 105
  18. lemma OAI.MainGap.cornerHer_entries line 125
  19. def OAI.MainGap.rowMatrix line 154
  20. lemma OAI.MainGap.rowMatrix_conjugate line 158
  21. lemma OAI.MainGap.finiteCuntzLE_corner_approx line 170
  22. lemma OAI.MainGap.regularTransport_diagonal line 176
  23. lemma OAI.MainGap.row_zero_of_self_star line 185
  24. lemma OAI.MainGap.col_zero_of_star_self line 195
  25. def OAI.MainGap.entryHer line 201
  26. lemma OAI.MainGap.entryHer_val line 204
  27. lemma OAI.MainGap.RegularTransport.carrier_entryHer line 211
  28. def OAI.MainGap.RegularTransport.slot line 240
  29. lemma OAI.MainGap.RegularTransport.slot_inner line 242
  30. lemma OAI.MainGap.RegularTransport.slot_outer_mem line 258
  31. lemma OAI.MainGap.RegularTransport.slot_mul line 266
  32. lemma OAI.MainGap.RegularTransport.slot_add line 277
  33. lemma OAI.MainGap.RegularTransport.slot_smul line 284
  34. lemma OAI.MainGap.RegularTransport.continuous_slot line 291
  35. def OAI.MainGap.RegularTransport.slotCLM line 298
  36. structure OAI.MainGap.OrthogonalSlots line 306
  37. theorem OAI.MainGap.orthogonalSlots_of_comparison line 313
  38. theorem OAI.MainGap.ProperlyInfinite.orthogonalSlots line 331
  39. lemma OAI.MainGap.OrthogonalSlots.represented_norm line 338
  40. lemma OAI.MainGap.OrthogonalSlots.norm_carrier line 345
  41. lemma OAI.MainGap.FiniteCuntzLE.double line 352
  42. lemma OAI.MainGap.finiteSum_cuntzLE line 360
  43. lemma OAI.MainGap.finiteSum_two_cuntzLE line 373
  44. lemma OAI.MainGap.finsetSum_cuntzLE line 377