OAI/GroupTheory/SimpleAmenable/CentralCovers/PrimitiveCentralLaws.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SimpleAmenable.InitialCoverSystem.PatchAtlas.primitive_full_central line 16
  2. theorem OAI.SimpleAmenable.InitialCoverSystem.PatchAtlas.primitive_family_law_all line 26
  3. theorem OAI.SimpleAmenable.primitive_laws_eventually line 49
  4. theorem OAI.SimpleAmenable.polygon_family_primitive_resolution line 65
  5. def OAI.SimpleAmenable.InitialCoverSystem.AllPrimitiveLaws line 81
  6. theorem OAI.SimpleAmenable.InitialCoverSystem.fullGeometricSector_independent line 87
  7. def OAI.SimpleAmenable.InitialCoverSystem.polygonStar line 100
  8. theorem OAI.SimpleAmenable.InitialCoverSystem.polygonStar_eq line 106
  9. theorem OAI.SimpleAmenable.InitialCoverSystem.polygonStar_projection line 113
  10. theorem OAI.SimpleAmenable.InitialCoverSystem.polygonStar_supported line 120
  11. theorem OAI.SimpleAmenable.InitialCoverSystem.polygonStar_whole line 126
  12. theorem OAI.SimpleAmenable.InitialCoverSystem.polygonStar_commute line 132
  13. theorem OAI.SimpleAmenable.InitialCoverSystem.polygonStar_union line 145
  14. theorem OAI.SimpleAmenable.InitialCoverSystem.polygonStars_finite_central line 162