OAI/Geometry/PeriodicTiling/ConstraintCycles.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PeriodicTilingThree.ordinaryCycle line 14
  2. def OAI.PeriodicTilingThree.ordinaryCycleLabels line 18
  3. def OAI.PeriodicTilingThree.seedCycle line 22
  4. theorem OAI.PeriodicTilingThree.seedCycle_zero line 34
  5. theorem OAI.PeriodicTilingThree.seedCycle_one line 39
  6. def OAI.PeriodicTilingThree.seedCycleLabels line 44
  7. theorem OAI.PeriodicTilingThree.seedCycleLabels_zero line 49
  8. theorem OAI.PeriodicTilingThree.seedCycleLabels_one line 54
  9. theorem OAI.PeriodicTilingThree.ordinaryCycle_exclusion_iff line 61
  10. theorem OAI.PeriodicTilingThree.seedCycle_exclusion_iff line 79
  11. def OAI.PeriodicTilingThree.wordConstraintTiles line 100
  12. def OAI.PeriodicTilingThree.seedConstraintTiles line 105
  13. theorem OAI.PeriodicTilingThree.nonempty_of_mem_wordConstraintTiles line 111
  14. theorem OAI.PeriodicTilingThree.nonempty_of_mem_seedConstraintTiles line 117
  15. theorem OAI.PeriodicTilingThree.wordConstraintTiles_iff line 124
  16. theorem OAI.PeriodicTilingThree.seedConstraintTiles_iff line 145