OAI/GroupTheory/SimpleAmenable/PolygonGeometry/OpenAffineCharts.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SimpleAmenable.openSquareChart line 16
  2. theorem OAI.SimpleAmenable.openSquareChart_open line 20
  3. theorem OAI.SimpleAmenable.openSquareChart_convex line 35
  4. theorem OAI.SimpleAmenable.self_mem_openSquareChart line 39
  5. theorem OAI.SimpleAmenable.openSquareChart_signs line 48
  6. theorem OAI.SimpleAmenable.squareArrangement_on_openChart line 59
  7. theorem OAI.SimpleAmenable.open_subset_closed_of_dense line 65
  8. theorem OAI.SimpleAmenable.open_translation_square line 74
  9. theorem OAI.SimpleAmenable.fullGroupAffineChart_square line 94
  10. def OAI.SimpleAmenable.chartCrossingParameter line 115
  11. theorem OAI.SimpleAmenable.chartCrossingParameter_spec line 118
  12. theorem OAI.SimpleAmenable.chartCrossingParameter_unique line 125
  13. theorem OAI.SimpleAmenable.openSquareChart_line_interval line 135