OAI/GroupTheory/SimpleAmenable/Amenability/LocalBarrierTransport.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SimpleAmenable.inFlagLattice_add line 15
2. theorem OAI.SimpleAmenable.mem_barrierSubdivision_interior line 23
3. theorem OAI.SimpleAmenable.barrierSubdivision_site_before_upper line 47
4. theorem OAI.SimpleAmenable.BarrierSignalSystem.local_line_transport line 65