OAI/GroupTheory/SimpleAmenable/PolygonGeometry/ObservableDistance.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SimpleAmenable.ObservableClose line 14
2. theorem OAI.SimpleAmenable.boundedObservable_integrable line 18
3. theorem OAI.SimpleAmenable.ObservableClose.mono line 25
4. theorem OAI.SimpleAmenable.ObservableClose.symm line 29
5. theorem OAI.SimpleAmenable.ObservableClose.map line 36
6. theorem OAI.SimpleAmenable.ObservableClose.event line 44
7. theorem OAI.SimpleAmenable.ObservableClose.prod_right line 53
8. theorem OAI.SimpleAmenable.observableClose_of_density line 73
9. theorem OAI.SimpleAmenable.infinitePi_split line 104