OAI/GroupTheory/SimpleAmenable/PolygonGeometry/SpatialChartGeometry.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SimpleAmenable.translated_clippedSlope_lift line 14
  2. theorem OAI.SimpleAmenable.clippedSlope_agree_on_rectangle line 32
  3. theorem OAI.SimpleAmenable.integralCutForm_tangent line 65
  4. theorem OAI.SimpleAmenable.integralCutForm_tangent_swapped line 69
  5. theorem OAI.SimpleAmenable.spatialTranslate_inter line 77
  6. theorem OAI.SimpleAmenable.spatialTranslate_compl line 81
  7. theorem OAI.SimpleAmenable.spatialTranslate_mono line 84
  8. theorem OAI.SimpleAmenable.spatialTranslate_resolved line 88
  9. theorem OAI.SimpleAmenable.spatialTranslate_coordinateInterval line 95
  10. theorem OAI.SimpleAmenable.spatialTranslate_coordinateRectangle line 110
  11. theorem OAI.SimpleAmenable.InitialCoverSystem.fullGeometricSector_shared_primitive line 122