OAI/GameTheory/SnakyTwentyOne/Semantics/Geometry.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.inverseOrientation line 8
  2. theorem OAI.SnakyPrototype.orient_inverse_left line 10
  3. theorem OAI.SnakyPrototype.orient_inverse_right line 13
  4. def OAI.SnakyPrototype.orientationEquiv line 16
  5. def OAI.SnakyPrototype.translationEquiv line 21
  6. def OAI.SnakyPrototype.placementEquiv line 26
  7. theorem OAI.SnakyPrototype.placementEquiv_apply line 28
  8. theorem OAI.SnakyPrototype.coe_placementEquiv line 30
  9. def OAI.SnakyPrototype.composeOrientation line 32
  10. theorem OAI.SnakyPrototype.orient_comp line 37
  11. theorem OAI.SnakyPrototype.orient_add line 41
  12. theorem OAI.SnakyPrototype.placement_comp line 45
  13. theorem OAI.SnakyPrototype.HasSnaky.mono line 49
  14. theorem OAI.SnakyPrototype.HasSnaky.placed line 53
  15. theorem OAI.SnakyPrototype.placed_template line 62
  16. def OAI.SnakyPrototype.basePoint line 69
  17. def OAI.SnakyPrototype.baseEnvelope line 70
  18. def OAI.SnakyPrototype.baseRequired line 72
  19. theorem OAI.SnakyPrototype.basePoint_mem line 73
  20. theorem OAI.SnakyPrototype.base_works line 75