OAI/GroupTheory/SimpleAmenable/CentralCovers/IndividualGridSplits.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SimpleAmenable.InitialCoverSystem.gridInput line 26
2. def OAI.SimpleAmenable.InitialCoverSystem.gridPiece line 30
3. theorem OAI.SimpleAmenable.InitialCoverSystem.gridPiece_supported line 34
4. theorem OAI.SimpleAmenable.InitialCoverSystem.gridPiece_control line 42
5. theorem OAI.SimpleAmenable.InitialCoverSystem.gridInput_split line 47
6. theorem OAI.SimpleAmenable.InitialCoverSystem.grid_complement_coherent line 60
7. theorem OAI.SimpleAmenable.InitialCoverSystem.gridInputs_normalize line 79
8. theorem OAI.SimpleAmenable.InitialCoverSystem.gridPieces_generate line 106
9. theorem OAI.SimpleAmenable.spatialTranslate_integral line 132
10. theorem OAI.SimpleAmenable.InitialCoverSystem.fullGeometricSector_shared_test line 147
11. theorem OAI.SimpleAmenable.InitialCoverSystem.tangentSign_integral line 173