OAI/GroupTheory/SimpleAmenable/PolygonGeometry/WindowCells.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SimpleAmenable.cutFraction line 15
  2. theorem OAI.SimpleAmenable.ordinary_cutFraction line 17
  3. theorem OAI.SimpleAmenable.endpointLabel_cutFraction line 21
  4. theorem OAI.SimpleAmenable.endpointLabel_labelTau line 25
  5. theorem OAI.SimpleAmenable.cutFraction_zero line 29
  6. def OAI.SimpleAmenable.windowEndpointSet line 32
  7. theorem OAI.SimpleAmenable.windowEndpointSet_card line 36
  8. def OAI.SimpleAmenable.cutOrdinaryOrder line 48
  9. def OAI.SimpleAmenable.windowInterior line 53
  10. theorem OAI.SimpleAmenable.windowInterior_mem line 56
  11. theorem OAI.SimpleAmenable.windowInterior_bounds line 59
  12. theorem OAI.SimpleAmenable.windowInterior_label line 67
  13. theorem OAI.SimpleAmenable.windowInterior_zero line 78
  14. def OAI.SimpleAmenable.windowCut line 95
  15. theorem OAI.SimpleAmenable.windowCut_zero line 98
  16. theorem OAI.SimpleAmenable.windowCut_last line 102
  17. theorem OAI.SimpleAmenable.windowCut_label line 106
  18. theorem OAI.SimpleAmenable.windowCut_strictMono line 117
  19. theorem OAI.SimpleAmenable.cutFraction_eq_self line 128
  20. theorem OAI.SimpleAmenable.cutFraction_label line 133
  21. theorem OAI.SimpleAmenable.windowEndpointSet_of_bounds line 141
  22. theorem OAI.SimpleAmenable.windowCut_bounds line 154
  23. theorem OAI.SimpleAmenable.windowCut_no_between line 165
  24. theorem OAI.SimpleAmenable.windowCut_mesh line 203