OAI/Geometry/PeriodicTiling/GraphTests.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PeriodicTilingThree.tiles_range_iff_unique_base line 14
  2. theorem OAI.PeriodicTilingThree.tiles_kernel_iff_unique_fibre line 54
  3. theorem OAI.PeriodicTilingThree.tiles_invariance_iff line 102
  4. def OAI.PeriodicTilingThree.usefulCoord line 153
  5. theorem OAI.PeriodicTilingThree.usefulCoord_apply line 158
  6. theorem OAI.PeriodicTilingThree.usefulCoord_point line 161
  7. theorem OAI.PeriodicTilingThree.kernel_horizontal_zero line 164
  8. instance OAI.PeriodicTilingThree.kernelFintype line 169
  9. def OAI.PeriodicTilingThree.kernelTile line 176
  10. theorem OAI.PeriodicTilingThree.mem_kernelTile line 179
  11. theorem OAI.PeriodicTilingThree.kernelTile_nonempty line 188
  12. def OAI.PeriodicTilingThree.baseLift line 191
  13. theorem OAI.PeriodicTilingThree.q0_baseLift line 193
  14. theorem OAI.PeriodicTilingThree.usefulCoord_baseLift line 196
  15. theorem OAI.PeriodicTilingThree.kernelTile_iff_unique_fibre line 199
  16. theorem OAI.PeriodicTilingThree.kernelTile_graph line 205
  17. theorem OAI.PeriodicTilingThree.kernelTile_iff_graph line 215
  18. def OAI.PeriodicTilingThree.invarianceZero line 240
  19. def OAI.PeriodicTilingThree.invarianceNonzero line 243
  20. def OAI.PeriodicTilingThree.invarianceTile line 246
  21. theorem OAI.PeriodicTilingThree.mem_invarianceTile line 250
  22. theorem OAI.PeriodicTilingThree.invarianceTile_nonempty line 278
  23. theorem OAI.PeriodicTilingThree.invarianceTile_disjoint line 283
  24. theorem OAI.PeriodicTilingThree.invarianceTile_card line 294
  25. theorem OAI.PeriodicTilingThree.invarianceTile_iff line 313