OAI/GroupTheory/SimpleAmenable/PolygonGeometry/FlagGerms.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SimpleAmenable.FlagDirections line 15
  2. theorem OAI.SimpleAmenable.flagDirections_sector line 18
  3. def OAI.SimpleAmenable.SquareBoundary line 46
  4. def OAI.SimpleAmenable.SquareFlag line 51
  5. theorem OAI.SimpleAmenable.sector_enters_square line 54
  6. theorem OAI.SimpleAmenable.squareSector_generic line 87
  7. def OAI.SimpleAmenable.IsSquareGerm line 96
  8. theorem OAI.SimpleAmenable.exists_squareGerm line 101
  9. theorem OAI.SimpleAmenable.IsSquareGerm.unique line 113
  10. def OAI.SimpleAmenable.flagValue line 121
  11. theorem OAI.SimpleAmenable.flagValue_spec line 125
  12. theorem OAI.SimpleAmenable.flagValue_eq line 129
  13. theorem OAI.SimpleAmenable.flagValue_map line 133
  14. theorem OAI.SimpleAmenable.flagValue_finite line 140
  15. def OAI.SimpleAmenable.flagMem line 150
  16. theorem OAI.SimpleAmenable.flagMem_iff line 154
  17. theorem OAI.SimpleAmenable.flagMem_bot line 165
  18. theorem OAI.SimpleAmenable.flagMem_sup line 173
  19. theorem OAI.SimpleAmenable.flagMem_compl line 182
  20. theorem OAI.SimpleAmenable.flagMem_halfPlane line 190