OAI/GroupTheory/SimpleAmenable/PolygonGeometry/PlaneStepFunctions.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SimpleAmenable.GenericPlane line 14
  2. def OAI.SimpleAmenable.GenericPlane.shift line 17
  3. theorem OAI.SimpleAmenable.GenericPlane.shift_zero line 19
  4. theorem OAI.SimpleAmenable.GenericPlane.shift_add line 22
  5. abbrev OAI.SimpleAmenable.PlaneCut line 29
  6. def OAI.SimpleAmenable.planeSign line 31
  7. def OAI.SimpleAmenable.HasPlaneArrangement line 34
  8. def OAI.SimpleAmenable.PlaneCompactSupport line 37
  9. def OAI.SimpleAmenable.planeStepSubmodule line 40
  10. abbrev OAI.SimpleAmenable.PlaneStep line 64
  11. theorem OAI.SimpleAmenable.PlaneStep.hasArrangement line 69
  12. theorem OAI.SimpleAmenable.PlaneStep.compactSupport line 70
  13. theorem OAI.SimpleAmenable.PlaneStep.translated_sign line 72
  14. theorem OAI.SimpleAmenable.PlaneStep.translated_arrangement line 83
  15. theorem OAI.SimpleAmenable.PlaneStep.translated_compact line 93
  16. def OAI.SimpleAmenable.PlaneStep.translate line 108
  17. theorem OAI.SimpleAmenable.PlaneStep.translate_apply line 114
  18. def OAI.SimpleAmenable.PlaneStep.representation line 117
  19. abbrev OAI.SimpleAmenable.PolygonGroupRing line 132
  20. def OAI.SimpleAmenable.PolygonCoefficientModule line 134
  21. instance OAI.SimpleAmenable.(instance at line 136) line 136
  22. instance OAI.SimpleAmenable.(instance at line 140) line 140
  23. def OAI.SimpleAmenable.TransverseDirection line 151
  24. def OAI.SimpleAmenable.planeSector line 154
  25. theorem OAI.SimpleAmenable.planeSector_open line 158
  26. theorem OAI.SimpleAmenable.planeSector_generic line 169
  27. def OAI.SimpleAmenable.arrangementNeighborhood line 190
  28. theorem OAI.SimpleAmenable.arrangementNeighborhood_open line 195
  29. theorem OAI.SimpleAmenable.self_mem_arrangementNeighborhood line 204
  30. theorem OAI.SimpleAmenable.planeSign_neighborhood line 213
  31. def OAI.SimpleAmenable.IsPlaneGerm line 238
  32. theorem OAI.SimpleAmenable.exists_planeGerm line 242
  33. theorem OAI.SimpleAmenable.IsPlaneGerm.unique line 253
  34. def OAI.SimpleAmenable.planeGerm line 261
  35. theorem OAI.SimpleAmenable.planeGerm_spec line 264
  36. theorem OAI.SimpleAmenable.planeGerm_eq line 269
  37. theorem OAI.SimpleAmenable.planeGerm_zero line 273
  38. theorem OAI.SimpleAmenable.planeGerm_add line 279
  39. theorem OAI.SimpleAmenable.planeGerm_smul line 289
  40. theorem OAI.SimpleAmenable.planeGerm_evaluate line 297
  41. theorem OAI.SimpleAmenable.planeGerm_congr_direction line 310