OAI/GroupTheory/SimpleAmenable/CentralCovers/PrimitiveGeometricGeneration.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SimpleAmenable.cutForm_sub line 15
  2. theorem OAI.SimpleAmenable.fract_small_lift line 19
  3. theorem OAI.SimpleAmenable.fract_small_lift_unique line 29
  4. theorem OAI.SimpleAmenable.mem_circularBoxPiece line 38
  5. theorem OAI.SimpleAmenable.mem_clippedSlope_lift line 47
  6. theorem OAI.SimpleAmenable.translated_clippedSlope_local line 84
  7. theorem OAI.SimpleAmenable.exists_cut_parameter line 96
  8. theorem OAI.SimpleAmenable.slope_line_anchor line 102
  9. def OAI.SimpleAmenable.ordinaryBox line 133
  10. def OAI.SimpleAmenable.genericBox line 136
  11. theorem OAI.SimpleAmenable.genericBox_eq line 139
  12. theorem OAI.SimpleAmenable.genericBox_mem line 151
  13. theorem OAI.SimpleAmenable.exists_box_in_open line 159
  14. theorem OAI.SimpleAmenable.halfPlane_locally_generated line 174
  15. theorem OAI.SimpleAmenable.slope_cuts_generated line 219