OAI/Geometry/PeriodicTiling/TilingTransport.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PeriodicTilingThree.Tiles.image_addEquiv line 14
  2. theorem OAI.PeriodicTilingThree.tiles_image_addEquiv_iff line 40
  3. theorem OAI.PeriodicTilingThree.addEquiv_image_symm_eq_preimage line 51
  4. theorem OAI.PeriodicTilingThree.Tiles.preimage_addEquiv line 55
  5. theorem OAI.PeriodicTilingThree.tiles_preimage_addEquiv_iff line 61
  6. theorem OAI.PeriodicTilingThree.Period.image line 73
  7. theorem OAI.PeriodicTilingThree.finiteIndex_map_of_surjective line 85
  8. theorem OAI.PeriodicTilingThree.FullyPeriodic.image_of_surjective line 93
  9. theorem OAI.PeriodicTilingThree.fullyPeriodic_image_addEquiv_iff line 102
  10. theorem OAI.PeriodicTilingThree.FullyPeriodic.preimage_addEquiv line 113
  11. theorem OAI.PeriodicTilingThree.fullyPeriodic_preimage_addEquiv_iff line 118
  12. theorem OAI.PeriodicTilingThree.finiteIndex_prod_bot line 129
  13. theorem OAI.PeriodicTilingThree.FullyPeriodic.prod_singleton_zero line 135