OAI/Geometry/PeriodicTiling/CommonSeedOutputs.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PeriodicTilingThree.seedOneSize line 15
  2. theorem OAI.PeriodicTilingThree.seedTwoSize line 20
  3. def OAI.PeriodicTilingThree.seedUseful line 25
  4. def OAI.PeriodicTilingThree.seedHigh line 35
  5. theorem OAI.PeriodicTilingThree.seedUseful_zero line 45
  6. theorem OAI.PeriodicTilingThree.seedUseful_one line 50
  7. theorem OAI.PeriodicTilingThree.seedHigh_zero line 55
  8. theorem OAI.PeriodicTilingThree.seedHigh_one line 60
  9. def OAI.PeriodicTilingThree.seedC line 65
  10. def OAI.PeriodicTilingThree.seedBeta line 68
  11. theorem OAI.PeriodicTilingThree.seedC_eq_of_residue_low line 71
  12. def OAI.PeriodicTilingThree.seedSourceInput line 76
  13. theorem OAI.PeriodicTilingThree.seedSourceInput_same line 79
  14. theorem OAI.PeriodicTilingThree.seedSourceInput_low line 84
  15. theorem OAI.PeriodicTilingThree.seed_source_residue line 89
  16. def OAI.PeriodicTilingThree.seedActualForward line 102
  17. theorem OAI.PeriodicTilingThree.seedActualForward_zero_eq line 109
  18. theorem OAI.PeriodicTilingThree.seedActualForward_one_eq line 120
  19. theorem OAI.PeriodicTilingThree.seedActualForward_bijective line 131
  20. theorem OAI.PeriodicTilingThree.both_seed_tests line 163
  21. def OAI.PeriodicTilingThree.seedActiveRegion line 168
  22. theorem OAI.PeriodicTilingThree.seedUseful_active_iff line 171