OAI/Geometry/Cannon/Energy/Plane.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CannonCharts.Plane line 22
  2. abbrev OAI.CannonCharts.SphereTwo line 24
  3. def OAI.CannonCharts.box line 26
  4. def OAI.CannonCharts.openBox line 28
  5. lemma OAI.CannonCharts.box_coords line 30
  6. lemma OAI.CannonCharts.openBox_coords line 34
  7. theorem OAI.CannonCharts.sphere_planar_chart line 38
  8. theorem OAI.CannonCharts.planar_chart line 56
  9. theorem OAI.CannonCharts.small_planar_chart line 62
  10. theorem OAI.CannonCharts.finite_small_charts line 93
  11. theorem OAI.CannonCharts.first_exit line 117
  12. theorem OAI.CannonCharts.continuous_lift line 141