OAI/Geometry/PeriodicTiling/Dependence.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PeriodicTilingThree.eq_of_update_invariant line 21
  2. theorem OAI.PeriodicTilingThree.eq_of_update_invariant_off line 31
  3. def OAI.PeriodicTilingThree.DigitActive line 55
  4. theorem OAI.PeriodicTilingThree.not_digitActive_iff line 58
  5. def OAI.PeriodicTilingThree.seedResidue line 66
  6. def OAI.PeriodicTilingThree.seedRepresentative line 69
  7. theorem OAI.PeriodicTilingThree.seedResidue_representative line 72
  8. def OAI.PeriodicTilingThree.usefulAt line 76
  9. def OAI.PeriodicTilingThree.ordinaryFactor line 79
  10. def OAI.PeriodicTilingThree.seedFactor line 83
  11. def OAI.PeriodicTilingThree.HasDependence line 87
  12. theorem OAI.PeriodicTilingThree.ordinaryFactor_spec line 93
  13. theorem OAI.PeriodicTilingThree.seedFactor_spec line 98
  14. theorem OAI.PeriodicTilingThree.usefulAt_factor line 103
  15. theorem OAI.PeriodicTilingThree.usefulAt_eq_of_lineValue_eq line 116
  16. theorem OAI.PeriodicTilingThree.usefulAt_eq_of_seedResidue_eq line 123
  17. def OAI.PeriodicTilingThree.Active line 130
  18. theorem OAI.PeriodicTilingThree.digitActive_iff_coordinates line 133
  19. theorem OAI.PeriodicTilingThree.no_digitActive_iff_constant line 140
  20. theorem OAI.PeriodicTilingThree.no_active_iff_constant line 159
  21. theorem OAI.PeriodicTilingThree.active_ordinary_iff line 163
  22. theorem OAI.PeriodicTilingThree.active_seed_iff line 171
  23. abbrev OAI.PeriodicTilingThree.DependenceIndex line 179
  24. def OAI.PeriodicTilingThree.lowGenerator line 183
  25. def OAI.PeriodicTilingThree.seedStep line 186
  26. def OAI.PeriodicTilingThree.dependenceChannel line 189
  27. def OAI.PeriodicTilingThree.dependenceShift line 194
  28. def OAI.PeriodicTilingThree.dependenceTile line 199
  29. theorem OAI.PeriodicTilingThree.dependenceTile_nonempty line 202
  30. theorem OAI.PeriodicTilingThree.dependenceTile_card line 206
  31. def OAI.PeriodicTilingThree.dependenceTiles line 210
  32. def OAI.PeriodicTilingThree.DependenceTests line 214
  33. def OAI.PeriodicTilingThree.DependenceInvariance line 217
  34. theorem OAI.PeriodicTilingThree.periodic_of_sub_eq line 221
  35. theorem OAI.PeriodicTilingThree.useful_update_of_generator line 226
  36. theorem OAI.PeriodicTilingThree.usefulAt_factor_of_generators line 242
  37. theorem OAI.PeriodicTilingThree.seedResidue_sub_step line 252
  38. theorem OAI.PeriodicTilingThree.dependenceInvariance_iff line 260
  39. theorem OAI.PeriodicTilingThree.dependenceTests_iff line 332
  40. theorem OAI.PeriodicTilingThree.dependenceTiles_iff line 339