OAI/GroupTheory/SimpleAmenable/PolygonGeometry/ResolvedBoolean.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SimpleAmenable.ResolvedBy line 17
  2. def OAI.SimpleAmenable.resolvedAlgebra line 20
  3. theorem OAI.SimpleAmenable.resolved_test line 33
  4. theorem OAI.SimpleAmenable.resolved_mono line 37
  5. def OAI.SimpleAmenable.resolvedPolygonMask line 46
  6. theorem OAI.SimpleAmenable.polygonAssignment_eq_iff line 50
  7. theorem OAI.SimpleAmenable.resolvedPolygonMask_mem line 62
  8. theorem OAI.SimpleAmenable.resolvedPolygonMask_mono line 73
  9. theorem OAI.SimpleAmenable.resolvedPolygonMask_disjoint line 79
  10. theorem OAI.SimpleAmenable.resolvedPolygonMask_union line 87
  11. theorem OAI.SimpleAmenable.coordinateShift_add line 103
  12. theorem OAI.SimpleAmenable.coordinateShift_neg line 107
  13. theorem OAI.SimpleAmenable.coordinateArc_tau line 111
  14. theorem OAI.SimpleAmenable.coordinate_preimage_add line 122
  15. def OAI.SimpleAmenable.coordinateBetween line 129
  16. theorem OAI.SimpleAmenable.coordinate_prefix_generated line 133
  17. theorem OAI.SimpleAmenable.coordinate_window_between_resolved line 165