OAI/Geometry/PeriodicTiling/ActivityWord.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PeriodicTilingThree.activeLabels line 12
  2. theorem OAI.PeriodicTilingThree.mem_activeLabels line 17
  3. def OAI.PeriodicTilingThree.selectSymbol line 23
  4. theorem OAI.PeriodicTilingThree.selectSymbol_mem line 27
  5. def OAI.PeriodicTilingThree.selectedWord line 35
  6. theorem OAI.PeriodicTilingThree.selectedWord_active line 38
  7. theorem OAI.PeriodicTilingThree.selectedWord_active_at line 46
  8. theorem OAI.PeriodicTilingThree.selectedWord_lineRule line 53
  9. theorem OAI.PeriodicTilingThree.selectedWord_nonconstant_of_forced_letters line 63
  10. theorem OAI.PeriodicTilingThree.graph_period_useful line 77
  11. theorem OAI.PeriodicTilingThree.activeLabels_eq_of_graph_period line 94
  12. theorem OAI.PeriodicTilingThree.selectedWord_period_of_graph_period line 104
  13. theorem OAI.PeriodicTilingThree.exists_positive_vertical_graph_period line 113