OAI/Geometry/PeriodicTiling/OneDimensional.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PeriodicTilingThree.oneDValue line 17
  2. theorem OAI.PeriodicTilingThree.oneDValue_injective line 19
  3. def OAI.PeriodicTilingThree.OneDConv line 25
  4. def OAI.PeriodicTilingThree.oneDWindow line 28
  5. def OAI.PeriodicTilingThree.OneDBlockEq line 31
  6. theorem OAI.PeriodicTilingThree.oneDBlockEq_of_window_eq line 34
  7. def OAI.PeriodicTilingThree.oneDIndicator line 42
  8. theorem OAI.PeriodicTilingThree.oneDConv_of_tiles line 46
  9. theorem OAI.PeriodicTilingThree.oneD_right_recurrence line 65
  10. theorem OAI.PeriodicTilingThree.oneD_left_recurrence line 76
  11. theorem OAI.PeriodicTilingThree.oneD_block_eq_add_one line 89
  12. theorem OAI.PeriodicTilingThree.oneD_block_eq_sub_one line 121
  13. theorem OAI.PeriodicTilingThree.oneD_block_eq_add_int line 152
  14. theorem OAI.PeriodicTilingThree.oneD_period_of_conv line 180
  15. theorem OAI.PeriodicTilingThree.periodic_of_tiles_int line 211
  16. theorem OAI.PeriodicTilingThree.fullyPeriodic_of_nat_period line 255
  17. theorem OAI.PeriodicTilingThree.fullyPeriodic_of_tiles_int line 270
  18. theorem OAI.PeriodicTilingThree.exists_fullyPeriodic_tiling_int line 276