OAI/GroupTheory/SimpleAmenable/PolygonGeometry/PolygonDiagramRefinement.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SimpleAmenable.PolygonObject.chart_target_track line 19
2. theorem OAI.SimpleAmenable.PolygonObject.targetTrack_fiber_polygon line 28
3. abbrev OAI.SimpleAmenable.PolygonObject.ArrowLabel line 51
4. instance OAI.SimpleAmenable.PolygonObject.arrowLabel_fintype line 54
5. def OAI.SimpleAmenable.PolygonObject.arrowLabel line 59
6. theorem OAI.SimpleAmenable.PolygonObject.arrowLabel_fiber_polygon line 62
7. def OAI.SimpleAmenable.PolygonObject.diagramLabel line 81
8. theorem OAI.SimpleAmenable.PolygonObject.diagramLabel_fiber_polygon line 84
9. theorem OAI.SimpleAmenable.PolygonObject.exists_common_arrow_refinement line 101