OAI/Analysis/CharacterCriterion/DropSections.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.KirchbergRordam.GenericRW.DropSections.Ix line 26
  2. abbrev OAI.KirchbergRordam.GenericRW.DropSections.Scalar line 27
  3. abbrev OAI.KirchbergRordam.GenericRW.DropSections.Mat line 28
  4. abbrev OAI.KirchbergRordam.GenericRW.DropSections.Small2 line 29
  5. abbrev OAI.KirchbergRordam.GenericRW.DropSections.Small3 line 30
  6. def OAI.KirchbergRordam.GenericRW.DropSections.entries line 33
  7. lemma OAI.KirchbergRordam.GenericRW.DropSections.entries_apply line 48
  8. def OAI.KirchbergRordam.GenericRW.DropSections.constMat line 52
  9. def OAI.KirchbergRordam.GenericRW.DropSections.leftConst line 65
  10. def OAI.KirchbergRordam.GenericRW.DropSections.rightConst line 67
  11. def OAI.KirchbergRordam.GenericRW.DropSections.times line 70
  12. lemma OAI.KirchbergRordam.GenericRW.DropSections.times_mul line 75
  13. lemma OAI.KirchbergRordam.GenericRW.DropSections.mul_times line 85
  14. lemma OAI.KirchbergRordam.GenericRW.DropSections.times_mul_left line 88
  15. lemma OAI.KirchbergRordam.GenericRW.DropSections.times_times line 91
  16. def OAI.KirchbergRordam.GenericRW.DropSections.leftPart line 94
  17. def OAI.KirchbergRordam.GenericRW.DropSections.rightPart line 95
  18. def OAI.KirchbergRordam.GenericRW.DropSections.endLeft line 98
  19. def OAI.KirchbergRordam.GenericRW.DropSections.endRight line 103
  20. lemma OAI.KirchbergRordam.GenericRW.DropSections.at_zero line 108
  21. lemma OAI.KirchbergRordam.GenericRW.DropSections.at_one line 121
  22. def OAI.KirchbergRordam.GenericRW.DropSections.weight line 136
  23. abbrev OAI.KirchbergRordam.GenericRW.DropSections.InteriorScalar line 137
  24. abbrev OAI.KirchbergRordam.GenericRW.DropSections.Interior line 138
  25. lemma OAI.KirchbergRordam.GenericRW.DropSections.weight_zero line 141
  26. def OAI.KirchbergRordam.GenericRW.DropSections.embed line 157
  27. lemma OAI.KirchbergRordam.GenericRW.DropSections.embed_injective line 162
  28. lemma OAI.KirchbergRordam.GenericRW.DropSections.embed_mul line 168
  29. lemma OAI.KirchbergRordam.GenericRW.DropSections.embed_star line 174
  30. lemma OAI.KirchbergRordam.GenericRW.DropSections.interior_at_zero line 176
  31. lemma OAI.KirchbergRordam.GenericRW.DropSections.interior_at_one line 179
  32. def OAI.KirchbergRordam.GenericRW.DropSections.residual line 182
  33. def OAI.KirchbergRordam.GenericRW.DropSections.interior line 187
  34. lemma OAI.KirchbergRordam.GenericRW.DropSections.decomposition line 206
  35. lemma OAI.KirchbergRordam.GenericRW.DropSections.endLeft_mul line 214
  36. lemma OAI.KirchbergRordam.GenericRW.DropSections.endRight_mul line 219
  37. lemma OAI.KirchbergRordam.GenericRW.DropSections.endLeft_one line 224
  38. lemma OAI.KirchbergRordam.GenericRW.DropSections.endRight_one line 229
  39. lemma OAI.KirchbergRordam.GenericRW.DropSections.endLeft_star line 234
  40. lemma OAI.KirchbergRordam.GenericRW.DropSections.endRight_star line 235
  41. lemma OAI.KirchbergRordam.GenericRW.DropSections.times_star line 237
  42. lemma OAI.KirchbergRordam.GenericRW.DropSections.leftPart_star line 242
  43. lemma OAI.KirchbergRordam.GenericRW.DropSections.rightPart_star line 248
  44. lemma OAI.KirchbergRordam.GenericRW.DropSections.interior_star line 254
  45. lemma OAI.KirchbergRordam.GenericRW.DropSections.interior_one line 260
  46. def OAI.KirchbergRordam.GenericRW.DropSections.weighted line 274
  47. lemma OAI.KirchbergRordam.GenericRW.DropSections.embed_weighted line 279
  48. def OAI.KirchbergRordam.GenericRW.DropSections.scalarMul line 281
  49. def OAI.KirchbergRordam.GenericRW.DropSections.actionLeft line 284
  50. def OAI.KirchbergRordam.GenericRW.DropSections.actionRight line 287
  51. lemma OAI.KirchbergRordam.GenericRW.DropSections.embed_actionLeft line 290
  52. lemma OAI.KirchbergRordam.GenericRW.DropSections.embed_actionRight line 298
  53. def OAI.KirchbergRordam.GenericRW.DropSections.actionLeftRev line 307
  54. def OAI.KirchbergRordam.GenericRW.DropSections.actionRightRev line 308
  55. lemma OAI.KirchbergRordam.GenericRW.DropSections.embed_actionLeftRev line 310
  56. lemma OAI.KirchbergRordam.GenericRW.DropSections.embed_actionRightRev line 315
  57. lemma OAI.KirchbergRordam.GenericRW.DropSections.leftPart_mul line 320
  58. lemma OAI.KirchbergRordam.GenericRW.DropSections.rightPart_mul line 330
  59. lemma OAI.KirchbergRordam.GenericRW.DropSections.leftConst_rightConst line 340
  60. lemma OAI.KirchbergRordam.GenericRW.DropSections.rightConst_leftConst line 345
  61. lemma OAI.KirchbergRordam.GenericRW.DropSections.leftPart_rightPart line 350
  62. lemma OAI.KirchbergRordam.GenericRW.DropSections.rightPart_leftPart line 356
  63. lemma OAI.KirchbergRordam.GenericRW.DropSections.interior_mul line 363