OAI/Geometry/PeriodicTiling/MarkedTileExistence.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PeriodicTilingThree.MarkedTile.periodEquiv line 10
  2. theorem OAI.PeriodicTilingThree.MarkedTile.periodEquiv_apply line 25
  3. theorem OAI.PeriodicTilingThree.MarkedTile.periodEquiv_symm_apply line 28
  4. def OAI.PeriodicTilingThree.MarkedTile.relocate line 31
  5. def OAI.PeriodicTilingThree.MarkedTile.ResidueSection.baseline line 49
  6. theorem OAI.PeriodicTilingThree.MarkedTile.ResidueSection.baseline_bijective line 53
  7. def OAI.PeriodicTilingThree.MarkedTile.ResidueSection.placement line 72
  8. theorem OAI.PeriodicTilingThree.MarkedTile.ResidueSection.placement_eq_baseline_relocate line 76
  9. theorem OAI.PeriodicTilingThree.MarkedTile.ResidueSection.placement_bijective line 92
  10. theorem OAI.PeriodicTilingThree.MarkedTile.ResidueSection.finalTile_tiles line 101
  11. theorem OAI.PeriodicTilingThree.MarkedTile.ResidueSection.cyclic_finalTile_tiles line 133