OAI/Geometry/PeriodicTiling/ResidueLiftPairs.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PeriodicTilingThree.PairGood line 9
  2. theorem OAI.PeriodicTilingThree.mem_PairGood line 15
  3. theorem OAI.PeriodicTilingThree.pairGood_assignment_iff line 22
  4. def OAI.PeriodicTilingThree.coordinateLiftPair line 28
  5. theorem OAI.PeriodicTilingThree.coordinateLiftPair_difference line 33
  6. theorem OAI.PeriodicTilingThree.coordinateLiftPair_injective line 39
  7. def OAI.PeriodicTilingThree.liftPairForDifference line 47
  8. theorem OAI.PeriodicTilingThree.liftPairForDifference_injective line 52
  9. theorem OAI.PeriodicTilingThree.liftPairForDifference_signed_sub line 61
  10. theorem OAI.PeriodicTilingThree.card_le_finset_of_injective line 69
  11. theorem OAI.PeriodicTilingThree.card_PairGood_ge line 80