OAI/GroupTheory/SimpleAmenable/PolygonGeometry/FiniteNestedLaw.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SimpleAmenable.prefix_range_le_differences line 17
  2. theorem OAI.SimpleAmenable.centralOn_of_nested_star_cuts line 35
  3. theorem OAI.SimpleAmenable.source_chart_containing_window line 60
  4. theorem OAI.SimpleAmenable.fixed_chart_margin_eventually line 81
  5. theorem OAI.SimpleAmenable.transverse_chart_margin_eventually line 88
  6. def OAI.SimpleAmenable.signQuadrantLower line 100
  7. def OAI.SimpleAmenable.signQuadrantUpper line 103
  8. theorem OAI.SimpleAmenable.signQuadrant_side line 106
  9. theorem OAI.SimpleAmenable.coordinateRectangle_mono line 141
  10. theorem OAI.SimpleAmenable.InitialCoverSystem.rectangle_control_from_axes line 155
  11. theorem OAI.SimpleAmenable.InitialCoverSystem.tangentSign_quadrant_control line 184