OAI/Analysis/CharacterCriterion/TensorSections.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.KirchbergRordam.PrimeTensorSections.continuous_starHom line 36
  2. abbrev OAI.KirchbergRordam.PrimeTensorSections.Square line 38
  3. abbrev OAI.KirchbergRordam.PrimeTensorSections.SquareFiber line 40
  4. def OAI.KirchbergRordam.PrimeTensorSections.leftSection line 42
  5. def OAI.KirchbergRordam.PrimeTensorSections.rightSection line 51
  6. lemma OAI.KirchbergRordam.PrimeTensorSections.sections_commute line 60
  7. def OAI.KirchbergRordam.PrimeTensorSections.sectionMap line 65
  8. lemma OAI.KirchbergRordam.PrimeTensorSections.sectionMap_left line 71
  9. lemma OAI.KirchbergRordam.PrimeTensorSections.sectionMap_right line 78
  10. lemma OAI.KirchbergRordam.PrimeTensorSections.sectionMap_tmul line 85
  11. lemma OAI.KirchbergRordam.PrimeTensorSections.scalarLeft_commute line 92
  12. lemma OAI.KirchbergRordam.PrimeTensorSections.scalarRight_commute line 100
  13. lemma OAI.KirchbergRordam.PrimeTensorSections.irreducible_left_evaluation line 108
  14. lemma OAI.KirchbergRordam.PrimeTensorSections.irreducible_right_evaluation line 114
  15. lemma OAI.KirchbergRordam.PrimeTensorSections.sectionMap_evaluation line 120
  16. lemma OAI.KirchbergRordam.PrimeTensorSections.irreducible_fiber_bound line 145
  17. theorem OAI.KirchbergRordam.PrimeTensorSections.sectionMap_injective line 160
  18. def OAI.KirchbergRordam.ContinuousSectionLocality.weight line 178
  19. lemma OAI.KirchbergRordam.ContinuousSectionLocality.weight_apply line 181
  20. theorem OAI.KirchbergRordam.ContinuousSectionLocality.mem_of_pointwise line 193
  21. def OAI.KirchbergRordam.ContinuousSectionLocality.scalarMap line 249
  22. lemma OAI.KirchbergRordam.ContinuousSectionLocality.scalarMap_apply line 258
  23. theorem OAI.KirchbergRordam.ContinuousSectionLocality.mem_of_pointwise_star line 267
  24. abbrev OAI.KirchbergRordam.ContinuousSectionLocality.Square line 282
  25. def OAI.KirchbergRordam.ContinuousSectionLocality.firstCoord line 283
  26. def OAI.KirchbergRordam.ContinuousSectionLocality.secondCoord line 284
  27. theorem OAI.KirchbergRordam.ContinuousSectionLocality.scalars_of_coordinates line 287
  28. lemma OAI.KirchbergRordam.PrimeTensorSections.sectionMap_isometry line 318
  29. def OAI.KirchbergRordam.PrimeTensorSections.sectionRange line 320
  30. lemma OAI.KirchbergRordam.PrimeTensorSections.sectionRange_closed line 322
  31. lemma OAI.KirchbergRordam.PrimeTensorSections.sectionRange_scalar line 325
  32. def OAI.KirchbergRordam.PrimeTensorSections.fiberRange line 342
  33. lemma OAI.KirchbergRordam.PrimeTensorSections.sectionMap_raw line 345
  34. lemma OAI.KirchbergRordam.PrimeTensorSections.fiberRange_lift line 356
  35. theorem OAI.KirchbergRordam.PrimeTensorSections.mem_sectionRange_of_fibers line 372
  36. def OAI.KirchbergRordam.PrimeDimensionDrop.leftRamp line 385
  37. def OAI.KirchbergRordam.PrimeDimensionDrop.rightRamp line 391
  38. lemma OAI.KirchbergRordam.PrimeDimensionDrop.evaluation_zero_range line 398
  39. lemma OAI.KirchbergRordam.PrimeDimensionDrop.evaluation_one_range line 405
  40. def OAI.KirchbergRordam.PrimeDimensionDrop.interiorRamp line 413
  41. lemma OAI.KirchbergRordam.PrimeDimensionDrop.evaluation_interior_surjective line 417
  42. lemma OAI.KirchbergRordam.PrimeDimensionDrop.evaluation_interior_range line 426
  43. def OAI.KirchbergRordam.MatrixTensor.tensorRange line 434
  44. lemma OAI.KirchbergRordam.MatrixTensor.tensorRange_tmul line 436
  45. lemma OAI.KirchbergRordam.MatrixTensor.tensorRange_left line 440
  46. lemma OAI.KirchbergRordam.MatrixTensor.tensorRange_right line 443
  47. lemma OAI.KirchbergRordam.MatrixTensor.tensorRange_mono line 446
  48. lemma OAI.KirchbergRordam.MatrixTensor.matrixUnit_kronecker line 454
  49. lemma OAI.KirchbergRordam.MatrixTensor.tensorRange_top_top line 463