OAI/Analysis/CharacterCriterion/InfiniteTensor.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KirchbergRordam.InfiniteMaxTensor.pack line 41
  2. abbrev OAI.KirchbergRordam.InfiniteMaxTensor.Stage line 44
  3. instance OAI.KirchbergRordam.InfiniteMaxTensor.stage_nontrivial line 45
  4. instance OAI.KirchbergRordam.InfiniteMaxTensor.stage_separable line 49
  5. def OAI.KirchbergRordam.InfiniteMaxTensor.chain line 55
  6. abbrev OAI.KirchbergRordam.InfiniteMaxTensor.system line 59
  7. abbrev OAI.KirchbergRordam.InfiniteMaxTensor.Algebra line 60
  8. instance OAI.KirchbergRordam.InfiniteMaxTensor.(instance at line 61) line 61
  9. instance OAI.KirchbergRordam.InfiniteMaxTensor.(instance at line 62) line 62
  10. instance OAI.KirchbergRordam.InfiniteMaxTensor.(instance at line 65) line 65
  11. def OAI.KirchbergRordam.InfiniteMaxTensor.inclusion line 69
  12. lemma OAI.KirchbergRordam.InfiniteMaxTensor.inclusion_isometry line 70
  13. lemma OAI.KirchbergRordam.InfiniteMaxTensor.inclusion_map line 71
  14. lemma OAI.KirchbergRordam.InfiniteMaxTensor.inclusion_step line 73
  15. def OAI.KirchbergRordam.InfiniteMaxTensor.tail line 79
  16. lemma OAI.KirchbergRordam.InfiniteMaxTensor.tail_commutes line 80
  17. def OAI.KirchbergRordam.InfiniteMaxTensor.sequenceHom line 85
  18. lemma OAI.KirchbergRordam.InfiniteMaxTensor.sequenceHom_apply line 95
  19. lemma OAI.KirchbergRordam.InfiniteMaxTensor.closed_commuting_preimage line 96
  20. lemma OAI.KirchbergRordam.InfiniteMaxTensor.central_tail line 99
  21. def OAI.KirchbergRordam.InfiniteMaxTensor.toCentral line 125
  22. theorem OAI.KirchbergRordam.InfiniteMaxTensor.central_no_character line 130
  23. abbrev OAI.KirchbergRordam.TensorHalfFlip.conj line 139
  24. def OAI.KirchbergRordam.TensorHalfFlip.HalfFlip line 141
  25. def OAI.KirchbergRordam.TensorHalfFlip.mapUnitary line 146
  26. lemma OAI.KirchbergRordam.TensorHalfFlip.conj_map line 148
  27. lemma OAI.KirchbergRordam.TensorHalfFlip.conj_mul line 151
  28. lemma OAI.KirchbergRordam.TensorHalfFlip.conj_fix line 153
  29. lemma OAI.KirchbergRordam.TensorHalfFlip.paired_conjugacy line 157
  30. theorem OAI.KirchbergRordam.TensorHalfFlip.tensor line 210
  31. lemma OAI.KirchbergRordam.CStarInductiveLimit.simultaneous_approximation line 228
  32. def OAI.KirchbergRordam.TensorHalfFlip.squareMap line 243
  33. lemma OAI.KirchbergRordam.TensorHalfFlip.squareMap_left line 246
  34. lemma OAI.KirchbergRordam.TensorHalfFlip.squareMap_right line 249
  35. lemma OAI.KirchbergRordam.TensorHalfFlip.norm_control_map line 252
  36. lemma OAI.KirchbergRordam.TensorHalfFlip.finite_of_halfFlip line 258
  37. theorem OAI.KirchbergRordam.TensorHalfFlip.inductive_limit line 271
  38. lemma OAI.KirchbergRordam.InfiniteMaxTensor.stage_halfFlip line 300
  39. theorem OAI.KirchbergRordam.InfiniteMaxTensor.halfFlip line 309
  40. lemma OAI.KirchbergRordam.NormUltrapower.map_central_of_equiv line 314
  41. lemma OAI.KirchbergRordam.NormUltrapower.map_equiv_inverse line 323
  42. theorem OAI.KirchbergRordam.central_isomorphism line 337
  43. theorem OAI.KirchbergRordam.minimal_tensor_central_right line 361
  44. lemma OAI.KirchbergRordam.InfiniteMaxTensor.stage_to_central line 420
  45. theorem OAI.KirchbergRordam.InfiniteMaxTensor.exists_central line 439
  46. theorem OAI.KirchbergRordam.infinite_balanced_character_criterion line 451