OAI/GroupTheory/SimpleAmenable/Amenability/BarrierStartGerm.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SimpleAmenable.continuous_nonzero_sign line 16
2. theorem OAI.SimpleAmenable.barrier_cut_difference line 26
3. theorem OAI.SimpleAmenable.barrier_start_cut_sign line 34
4. theorem OAI.SimpleAmenable.flagValue_of_arrangement_signs line 75
5. theorem OAI.SimpleAmenable.flagAffineData_barrier_chart line 93