OAI/GroupTheory/SimpleAmenable/Amenability/FinitePartitionArrows.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SimpleAmenable.PartitionArrow.cellMap line 20
2. theorem OAI.SimpleAmenable.PartitionArrow.cellMap_image line 23
3. theorem OAI.SimpleAmenable.PartitionArrow.eq_of_cellMap line 26
4. instance OAI.SimpleAmenable.PartitionArrow.arrows_finite line 63
5. def OAI.SimpleAmenable.BarrierSignalSystem.sampledPartition line 76
6. theorem OAI.SimpleAmenable.generic_component_image line 81
7. theorem OAI.SimpleAmenable.BarrierMenu.component_chart line 120
8. theorem OAI.SimpleAmenable.BarrierMenu.sampledPartition_arrow line 134