OAI/GroupTheory/SimpleAmenable/PolygonGeometry/PolygonArea.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SimpleAmenable.continuous_cutForm line 18
  2. theorem OAI.SimpleAmenable.measurableSet_avoidsCuts line 22
  3. theorem OAI.SimpleAmenable.volume_cut_level line 31
  4. theorem OAI.SimpleAmenable.ae_avoidsCuts line 56
  5. theorem OAI.SimpleAmenable.measurableSet_genericSquare line 64
  6. theorem OAI.SimpleAmenable.volume_genericSquare line 69
  7. def OAI.SimpleAmenable.PolygonArea.square line 89
  8. theorem OAI.SimpleAmenable.PolygonArea.null_frontier_inter line 91
  9. theorem OAI.SimpleAmenable.PolygonArea.null_frontier_union line 98
  10. theorem OAI.SimpleAmenable.PolygonArea.null_frontier_diff line 105
  11. theorem OAI.SimpleAmenable.PolygonArea.null_frontier_cut line 111
  12. theorem OAI.SimpleAmenable.PolygonArea.null_frontier_square line 117
  13. theorem OAI.SimpleAmenable.PolygonArea.representative line 127
  14. def OAI.SimpleAmenable.PolygonArea.area line 155
  15. theorem OAI.SimpleAmenable.PolygonArea.image_eq_rep line 158
  16. theorem OAI.SimpleAmenable.PolygonArea.area_eq_rep line 169
  17. theorem OAI.SimpleAmenable.PolygonArea.measurable_image line 177
  18. theorem OAI.SimpleAmenable.PolygonArea.area_le_one line 183
  19. theorem OAI.SimpleAmenable.PolygonArea.area_top line 190
  20. theorem OAI.SimpleAmenable.PolygonArea.closure_ae_eq line 201
  21. theorem OAI.SimpleAmenable.PolygonArea.interior_ae_eq line 215