OAI/GroupTheory/SimpleAmenable/PolygonGeometry/InwardGermTransport.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.SimpleAmenable.ConcurrentGeometry.InwardChart.germ_ruleline 15 - theorem
OAI.SimpleAmenable.ConcurrentGeometry.InwardChart.polygons_cut_on_marginline 28 - theorem
OAI.SimpleAmenable.ConcurrentGeometry.InwardChart.model_mem_iff_germ_ruleline 40 - theorem
OAI.SimpleAmenable.local_periodic_intervalline 61 - theorem
OAI.SimpleAmenable.local_periodic_rectangleline 99 - theorem
OAI.SimpleAmenable.local_clipped_formulaline 129