OAI/GroupTheory/SimpleAmenable/PolygonGeometry/FrameDisjointness.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SimpleAmenable.OffsetFrame.restrict line 17
2. theorem OAI.SimpleAmenable.InitialCoverSystem.polygonStar_alphabet_aligned line 31
3. theorem OAI.SimpleAmenable.InitialCoverSystem.frameStar_subalphabet line 46
4. theorem OAI.SimpleAmenable.InitialCoverSystem.frameStar_disjoint_alphabets line 56
5. theorem OAI.SimpleAmenable.supported_fixer_commute line 96
6. theorem OAI.SimpleAmenable.conditional_alphabet_supported line 104
7. def OAI.SimpleAmenable.frameDomain line 119
8. theorem OAI.SimpleAmenable.InitialCoverSystem.frameStar_supported line 129
9. theorem OAI.SimpleAmenable.InitialCoverSystem.polygonStars_pointwise_fixer line 148