OAI/Analysis/CharacterCriterion/CubeCalculus.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KirchbergRordam.GenericRW.JointCalculus.coordinates line 30
  2. def OAI.KirchbergRordam.GenericRW.JointCalculus.hom line 35
  3. def OAI.KirchbergRordam.GenericRW.JointCalculus.coordinate line 38
  4. lemma OAI.KirchbergRordam.GenericRW.JointCalculus.hom_coordinate line 41
  5. def OAI.KirchbergRordam.GenericRW.CentralCalculus.center line 66
  6. instance OAI.KirchbergRordam.GenericRW.CentralCalculus.centerClosed line 67
  7. instance OAI.KirchbergRordam.GenericRW.CentralCalculus.centerComm line 70
  8. def OAI.KirchbergRordam.GenericRW.CentralCalculus.inclusion line 73
  9. lemma OAI.KirchbergRordam.GenericRW.CentralCalculus.mem_center line 76
  10. lemma OAI.KirchbergRordam.GenericRW.CentralCalculus.commute line 86
  11. def OAI.KirchbergRordam.GenericRW.CentralCalculus.family line 96
  12. def OAI.KirchbergRordam.GenericRW.CentralCalculus.hom line 98
  13. lemma OAI.KirchbergRordam.GenericRW.CentralCalculus.hom_coordinate line 100
  14. lemma OAI.KirchbergRordam.GenericRW.CentralCalculus.hom_commute line 105
  15. def OAI.KirchbergRordam.GenericRW.CubeCalculus.coord line 111
  16. lemma OAI.KirchbergRordam.GenericRW.CubeCalculus.ext_coord line 114
  17. lemma OAI.KirchbergRordam.GenericRW.CubeFrame.term_norm line 154
  18. def OAI.KirchbergRordam.GenericRW.CubeFrame.expansion line 180
  19. lemma OAI.KirchbergRordam.GenericRW.CubeFrame.coefficient line 188
  20. lemma OAI.KirchbergRordam.GenericRW.CubeFrame.expansion_norm line 216
  21. theorem OAI.KirchbergRordam.GenericRW.CubeFrame.faithful line 234
  22. lemma OAI.KirchbergRordam.GenericRW.CubeFrame.closed_range line 247
  23. def OAI.KirchbergRordam.GenericRW.CubeFrame.scalarSection line 256
  24. lemma OAI.KirchbergRordam.GenericRW.CubeFrame.scalarSection_continuous line 263
  25. lemma OAI.KirchbergRordam.GenericRW.CubeFrame.coefficient_mem_range line 282
  26. theorem OAI.KirchbergRordam.GenericRW.CubeFrame.section_mem_range line 305
  27. theorem OAI.KirchbergRordam.GenericRW.CubeFrame.exists_unique_lift line 324