OAI/Analysis/CharacterCriterion/BalancedLimit.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.KirchbergRordam.M2 line 34
  2. abbrev OAI.KirchbergRordam.M3 line 35
  3. abbrev OAI.KirchbergRordam.M6 line 36
  4. def OAI.KirchbergRordam.leftMatrixAlgebra line 39
  5. def OAI.KirchbergRordam.rightMatrixAlgebra line 56
  6. def OAI.KirchbergRordam.leftMatrix line 73
  7. def OAI.KirchbergRordam.rightMatrix line 78
  8. def OAI.KirchbergRordam.matrixEval line 83
  9. def OAI.KirchbergRordam.dimensionDropSubalgebra line 93
  10. instance OAI.KirchbergRordam.(instance at line 96) line 96
  11. instance OAI.KirchbergRordam.dimensionDropClosed line 99
  12. abbrev OAI.KirchbergRordam.DimensionDrop23 line 109
  13. instance OAI.KirchbergRordam.dropSubringClass line 111
  14. instance OAI.KirchbergRordam.(instance at line 115) line 115
  15. example OAI.KirchbergRordam.(example at line 117) line 117
  16. def OAI.KirchbergRordam.dropCoordinate line 120
  17. def OAI.KirchbergRordam.leftCone line 130
  18. def OAI.KirchbergRordam.rightCone line 142
  19. def OAI.KirchbergRordam.matrixUnit line 154
  20. theorem OAI.KirchbergRordam.drop_ext line 158
  21. theorem OAI.KirchbergRordam.matrixUnit_mul line 164
  22. theorem OAI.KirchbergRordam.matrixUnit_mul_self line 170
  23. theorem OAI.KirchbergRordam.leftCone_mul_self line 175
  24. theorem OAI.KirchbergRordam.rightCone_mul_self line 183
  25. theorem OAI.KirchbergRordam.matrixUnit_two_diagonal line 191
  26. theorem OAI.KirchbergRordam.matrixUnit_three_diagonal line 199
  27. theorem OAI.KirchbergRordam.drop_left_identity line 207
  28. theorem OAI.KirchbergRordam.drop_right_identity line 222
  29. theorem OAI.KirchbergRordam.dimensionDrop23_no_ringhom line 239
  30. theorem OAI.KirchbergRordam.dimensionDrop23_no_character line 261
  31. abbrev OAI.KirchbergRordam.BalancedDropLimit.Stage line 271
  32. instance OAI.KirchbergRordam.BalancedDropLimit.(instance at line 272) line 272
  33. instance OAI.KirchbergRordam.BalancedDropLimit.(instance at line 273) line 273
  34. instance OAI.KirchbergRordam.BalancedDropLimit.(instance at line 274) line 274
  35. def OAI.KirchbergRordam.BalancedDropLimit.chain line 276
  36. abbrev OAI.KirchbergRordam.BalancedDropLimit.system line 281
  37. instance OAI.KirchbergRordam.BalancedDropLimit.(instance at line 282) line 282
  38. instance OAI.KirchbergRordam.BalancedDropLimit.(instance at line 285) line 285
  39. abbrev OAI.KirchbergRordam.BalancedDropLimit.Algebra line 289
  40. instance OAI.KirchbergRordam.BalancedDropLimit.(instance at line 290) line 290
  41. instance OAI.KirchbergRordam.BalancedDropLimit.(instance at line 291) line 291
  42. instance OAI.KirchbergRordam.BalancedDropLimit.(instance at line 292) line 292
  43. def OAI.KirchbergRordam.BalancedDropLimit.inclusion line 294
  44. lemma OAI.KirchbergRordam.BalancedDropLimit.norm_inclusion line 295
  45. lemma OAI.KirchbergRordam.BalancedDropLimit.inclusion_isometry line 297
  46. lemma OAI.KirchbergRordam.BalancedDropLimit.inclusion_step line 299
  47. def OAI.KirchbergRordam.BalancedDropLimit.initial line 310
  48. theorem OAI.KirchbergRordam.BalancedDropLimit.no_character line 312
  49. lemma OAI.KirchbergRordam.BalancedDropLimit.denseRange_inclusion line 315
  50. lemma OAI.KirchbergRordam.CStarInductiveLimit.quotient_eq_of_eventuallyEq line 326
  51. def OAI.KirchbergRordam.CStarInductiveLimit.stageSeq line 335
  52. lemma OAI.KirchbergRordam.CStarInductiveLimit.stageSeq_apply line 344
  53. def OAI.KirchbergRordam.CStarInductiveLimit.stageHom line 348
  54. lemma OAI.KirchbergRordam.CStarInductiveLimit.stageHom_map line 386
  55. def OAI.KirchbergRordam.CStarInductiveLimit.toUltrapower line 395
  56. lemma OAI.KirchbergRordam.CStarInductiveLimit.toUltrapower_of line 400
  57. theorem OAI.KirchbergRordam.CStarInductiveLimit.exists_toCentral line 405
  58. lemma OAI.KirchbergRordam.BalancedDropMultiplicity.stage_power line 417
  59. lemma OAI.KirchbergRordam.BalancedDropMultiplicity.stage_power_successor line 423
  60. theorem OAI.KirchbergRordam.BalancedDropLimit.stage_to_central line 433
  61. theorem OAI.KirchbergRordam.BalancedDropLimit.to_central line 443