OAI/GroupTheory/SimpleAmenable/PolygonGeometry/ClosedChartOverlap.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SimpleAmenable.planar_lift_avoidsCuts line 14
  2. theorem OAI.SimpleAmenable.coordinateRectangle_strict_lift line 29
  3. theorem OAI.SimpleAmenable.clippedSlope_agree_on_closed_rectangle line 43
  4. def OAI.SimpleAmenable.orderedCutMax line 80
  5. def OAI.SimpleAmenable.orderedCutMin line 82
  6. theorem OAI.SimpleAmenable.ordinary_orderedCutMax line 85
  7. theorem OAI.SimpleAmenable.ordinary_orderedCutMin line 92
  8. def OAI.SimpleAmenable.clippingOverlapLower line 99
  9. def OAI.SimpleAmenable.clippingOverlapUpper line 101
  10. theorem OAI.SimpleAmenable.clippingOverlap_bounds line 104
  11. theorem OAI.SimpleAmenable.exists_full_overlap_window line 123
  12. theorem OAI.SimpleAmenable.InitialCoverSystem.tangentSign_step_action_closed line 144