OAI/GroupTheory/SimpleAmenable/Amenability/BarrierChartRefinement.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SimpleAmenable.barrierComponent_cut_sign line 15
2. theorem OAI.SimpleAmenable.BarrierSignalSystem.component_cut_sign line 40
3. theorem OAI.SimpleAmenable.BarrierSignalSystem.component_step_eventually line 56
4. theorem OAI.SimpleAmenable.BarrierSignalSystem.component_affine_eventually line 77
5. theorem OAI.SimpleAmenable.barrierIntersection_lattice line 94
6. def OAI.SimpleAmenable.barrierInteriorSite line 103
7. theorem OAI.SimpleAmenable.BarrierSignalSystem.crossing_in_subdivision line 115
8. theorem OAI.SimpleAmenable.barrierLineParameter_add line 144
9. theorem OAI.SimpleAmenable.barrierLinePoint_translate line 148