OAI/Geometry/PeriodicTiling/SharedSeedSizeTransport.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PeriodicTilingThree.SharedSeed.usefulOneOfEq line 14
  2. def OAI.PeriodicTilingThree.SharedSeed.highOneOfEq line 19
  3. def OAI.PeriodicTilingThree.SharedSeed.usefulTwoOfEq line 24
  4. def OAI.PeriodicTilingThree.SharedSeed.highTwoOfEq line 29
  5. def OAI.PeriodicTilingThree.SharedSeed.oneForwardOfEq line 34
  6. def OAI.PeriodicTilingThree.SharedSeed.twoForwardOfEq line 42
  7. theorem OAI.PeriodicTilingThree.SharedSeed.oneForwardOfEq_bijective line 50
  8. theorem OAI.PeriodicTilingThree.SharedSeed.twoForwardOfEq_bijective line 61
  9. theorem OAI.PeriodicTilingThree.SharedSeed.usefulOneOfEq_active line 72
  10. theorem OAI.PeriodicTilingThree.SharedSeed.usefulTwoOfEq_active line 83
  11. theorem OAI.PeriodicTilingThree.SharedSeed.usefulOneOfEq_inactive_eq line 94
  12. theorem OAI.PeriodicTilingThree.SharedSeed.usefulTwoOfEq_inactive_eq line 106
  13. theorem OAI.PeriodicTilingThree.SharedSeed.usefulOneOfEq_activity_iff line 118
  14. theorem OAI.PeriodicTilingThree.SharedSeed.usefulTwoOfEq_activity_iff line 132