OAI/GroupTheory/SimpleAmenable/PolygonGeometry/PolygonBankEmbedding.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.SimpleAmenable.PolygonObject.BankEmbedding line 17
2. instance OAI.SimpleAmenable.PolygonObject.BankEmbedding.(instance at line 23) line 23
3. theorem OAI.SimpleAmenable.PolygonObject.BankEmbedding.injective line 25
4. theorem OAI.SimpleAmenable.PolygonObject.BankEmbedding.range_fiber_polygon line 27
5. def OAI.SimpleAmenable.PolygonObject.BankEmbedding.imageBank line 62
6. theorem OAI.SimpleAmenable.PolygonObject.BankEmbedding.imageBank_area_le line 65
7. theorem OAI.SimpleAmenable.PolygonObject.BankEmbedding.exists_into line 132
8. def OAI.SimpleAmenable.PolygonObject.BankEmbedding.inclusion line 149
9. theorem OAI.SimpleAmenable.PolygonObject.BankEmbedding.exists_away line 152
10. theorem OAI.SimpleAmenable.PolygonObject.BankEmbedding.cycle_three line 196