OAI/Geometry/PeriodicTiling/CycleTests.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PeriodicTilingThree.cycleExtend line 23
  2. theorem OAI.PeriodicTilingThree.cycleExtend_apply line 27
  3. theorem OAI.PeriodicTilingThree.cycleExtend_eq_zero line 41
  4. def OAI.PeriodicTilingThree.cycleShift line 53
  5. theorem OAI.PeriodicTilingThree.cycleShift_apply line 57
  6. theorem OAI.PeriodicTilingThree.cycleShift_eq_zero line 67
  7. def OAI.PeriodicTilingThree.cycleMap line 77
  8. theorem OAI.PeriodicTilingThree.cycleMap_apply_cycle line 82
  9. theorem OAI.PeriodicTilingThree.forall_of_cyclic_step line 90
  10. theorem OAI.PeriodicTilingThree.cycleMap_injective_of_inactive line 101
  11. theorem OAI.PeriodicTilingThree.cycleMap_bijective_of_inactive line 145
  12. theorem OAI.PeriodicTilingThree.cycleMap_collision_of_all_active line 153
  13. theorem OAI.PeriodicTilingThree.forall_cycleMap_bijective_iff line 192
  14. theorem OAI.PeriodicTilingThree.existsUnique_fixed_comp_iff line 211
  15. theorem OAI.PeriodicTilingThree.tiles_offset_iff_permutation line 231
  16. def OAI.PeriodicTilingThree.usefulProjection line 270
  17. theorem OAI.PeriodicTilingThree.usefulProjection_apply line 275
  18. theorem OAI.PeriodicTilingThree.usefulProjection_point line 278
  19. theorem OAI.PeriodicTilingThree.q0_usefulProjection_surjective line 281
  20. theorem OAI.PeriodicTilingThree.offset_horizontal_zero line 288
  21. instance OAI.PeriodicTilingThree.offsetFintype line 292
  22. def OAI.PeriodicTilingThree.offsetTile line 300
  23. theorem OAI.PeriodicTilingThree.mem_offsetTile line 304
  24. theorem OAI.PeriodicTilingThree.offsetTile_nonempty line 313
  25. theorem OAI.PeriodicTilingThree.offsetTile_iff line 318
  26. def OAI.PeriodicTilingThree.cycleTile line 338
  27. theorem OAI.PeriodicTilingThree.cycleTile_nonempty line 344
  28. theorem OAI.PeriodicTilingThree.cycleTile_iff line 349
  29. theorem OAI.PeriodicTilingThree.all_cycleTile_iff line 368
  30. def OAI.PeriodicTilingThree.cycleTiles line 388
  31. theorem OAI.PeriodicTilingThree.cycleTiles_nonempty line 393
  32. theorem OAI.PeriodicTilingThree.nonempty_of_mem_cycleTiles line 399
  33. theorem OAI.PeriodicTilingThree.forall_mem_cycleTiles_iff line 406
  34. theorem OAI.PeriodicTilingThree.cycle_exclusion_iff line 420