OAI/Geometry/Cannon/Energy/LiftPath.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CannonChart.liftPath line 25
  2. lemma OAI.CannonChart.liftPath_apply line 36
  3. lemma OAI.CannonChart.lift_joinedIn line 42
  4. instance OAI.CannonLevel.(instance at line 58) line 58
  5. theorem OAI.CannonLevel.regularized_values line 61
  6. theorem OAI.CannonLevel.separating_level line 81
  7. lemma OAI.CannonLevel.slab_pathConnected line 138
  8. def OAI.CannonLevel.topBand line 156
  9. def OAI.CannonLevel.bottomBand line 158
  10. def OAI.CannonLevel.centralRectangle line 160
  11. lemma OAI.CannonLevel.topBand_pathConnected line 162
  12. lemma OAI.CannonLevel.bottomBand_pathConnected line 167
  13. theorem OAI.CannonLevel.rectangle_separating_level line 172