OAI/Analysis/CharacterCriterion/MinimalFunctoriality.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KirchbergRordam.Spatial.flipL line 41
  2. lemma OAI.KirchbergRordam.Spatial.flipL_coe line 43
  3. lemma OAI.KirchbergRordam.Spatial.flipL_flipL line 46
  4. lemma OAI.KirchbergRordam.Spatial.norm_flipL line 50
  5. def OAI.KirchbergRordam.Spatial.flip line 54
  6. lemma OAI.KirchbergRordam.Spatial.flip_coe line 60
  7. lemma OAI.KirchbergRordam.Spatial.flip_symm line 62
  8. lemma OAI.KirchbergRordam.Spatial.flip_map line 63
  9. lemma OAI.KirchbergRordam.Spatial.norm_flip_conjugate line 73
  10. def OAI.KirchbergRordam.MinTensor.algebraicFlip line 84
  11. lemma OAI.KirchbergRordam.MinTensor.algebraicFlip_tmul line 89
  12. lemma OAI.KirchbergRordam.MinTensor.algebraicFlip_flip line 90
  13. def OAI.KirchbergRordam.MinTensor.RepresentationPair.rawMap line 93
  14. lemma OAI.KirchbergRordam.MinTensor.RepresentationPair.rawMap_tmul line 96
  15. def OAI.KirchbergRordam.MinTensor.RepresentationPair.swap line 98
  16. lemma OAI.KirchbergRordam.MinTensor.liftRaw_conjugate_swap line 109
  17. lemma OAI.KirchbergRordam.MinTensor.swap_left_flip line 124
  18. lemma OAI.KirchbergRordam.MinTensor.swap_right_flip line 127
  19. lemma OAI.KirchbergRordam.MinTensor.liftRaw_swap line 130
  20. lemma OAI.KirchbergRordam.MinTensor.crossSeminorm_apply line 148
  21. lemma OAI.KirchbergRordam.MinTensor.crossSeminorm_swap line 150
  22. lemma OAI.KirchbergRordam.MinTensor.seminorm_algebraicFlip_le line 155
  23. lemma OAI.KirchbergRordam.MinTensor.seminorm_algebraicFlip line 162
  24. def OAI.KirchbergRordam.MinTensor.flipRaw line 165
  25. lemma OAI.KirchbergRordam.MinTensor.norm_flipRaw line 167
  26. lemma OAI.KirchbergRordam.MinTensor.continuous_flipRaw line 171
  27. def OAI.KirchbergRordam.MinTensor.flipHom line 176
  28. lemma OAI.KirchbergRordam.MinTensor.flipHom_of line 195
  29. lemma OAI.KirchbergRordam.MinTensor.flipHom_includeLeft line 197
  30. lemma OAI.KirchbergRordam.MinTensor.flipHom_includeRight line 201
  31. lemma OAI.KirchbergRordam.MinTensor.flipHom_flipHom line 205
  32. def OAI.KirchbergRordam.MinTensor.flip line 217
  33. lemma OAI.KirchbergRordam.MinTensor.flip_includeLeft line 220
  34. lemma OAI.KirchbergRordam.MinTensor.flip_includeRight line 222