OAI/Geometry/PeriodicTiling/CyclicCoordinates.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PeriodicTilingThree.low line 12
  2. abbrev OAI.PeriodicTilingThree.highMul line 15
  3. abbrev OAI.PeriodicTilingThree.shear line 18
  4. abbrev OAI.PeriodicTilingThree.shearEquiv line 21
  5. theorem OAI.PeriodicTilingThree.low_shear line 25
  6. theorem OAI.PeriodicTilingThree.highMul_injective line 28
  7. theorem OAI.PeriodicTilingThree.low_highMul line 31
  8. theorem OAI.PeriodicTilingThree.shear_injective line 34
  9. theorem OAI.PeriodicTilingThree.shear_add line 37
  10. theorem OAI.PeriodicTilingThree.shear_source_add line 42
  11. def OAI.PeriodicTilingThree.q0 line 47
  12. theorem OAI.PeriodicTilingThree.q0_apply line 60
  13. def OAI.PeriodicTilingThree.point line 65
  14. theorem OAI.PeriodicTilingThree.point_horizontal line 68
  15. theorem OAI.PeriodicTilingThree.point_z line 69
  16. theorem OAI.PeriodicTilingThree.point_c line 70
  17. theorem OAI.PeriodicTilingThree.point_v line 72
  18. theorem OAI.PeriodicTilingThree.q0_point line 75
  19. theorem OAI.PeriodicTilingThree.point_injective line 81
  20. def OAI.PeriodicTilingThree.graph line 86
  21. theorem OAI.PeriodicTilingThree.point_mem_graph line 88
  22. theorem OAI.PeriodicTilingThree.eq_point_of_mem_graph line 91
  23. def OAI.PeriodicTilingThree.zeroOutputs line 96
  24. theorem OAI.PeriodicTilingThree.q0_surjective line 99
  25. theorem OAI.PeriodicTilingThree.section_low line 103
  26. def OAI.PeriodicTilingThree.outputsOfSection line 107
  27. theorem OAI.PeriodicTilingThree.point_outputsOfSection line 113
  28. theorem OAI.PeriodicTilingThree.graph_outputsOfSection line 126