OAI/Geometry/Cannon/PlanarGraphs/GraphShear.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CannonPlanarCorner.graphShear line 32
  2. lemma OAI.CannonPlanarCorner.graphShear_apply line 40
  3. def OAI.CannonPlanarCorner.bendHeight line 43
  4. lemma OAI.CannonPlanarCorner.bendHeight_nonpos line 46
  5. lemma OAI.CannonPlanarCorner.bendHeight_nonneg line 48
  6. lemma OAI.CannonPlanarCorner.complex_real_inner line 51
  7. theorem OAI.CannonPlanarCorner.separating_multiplier line 55
  8. def OAI.CannonPlanarCorner.ray line 89
  9. def OAI.CannonPlanarCorner.horizontal line 91
  10. theorem OAI.CannonPlanarCorner.flattened_bend line 93
  11. theorem OAI.CannonPlanarCorner.straighten_corner line 132
  12. lemma OAI.CannonPlanarCorner.local_ray_segment line 161