OAI/MathematicalPhysics/PEPSSubvolume/RectangleTiling.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Exact clipped-square lattice tilings and geometric weights.

  1. theorem OAI.PolynomialPEPS.Subvolume.RectangleTiling.interval_index line 26
  2. theorem OAI.PolynomialPEPS.Subvolume.RectangleTiling.interval_unique line 44
  3. theorem OAI.PolynomialPEPS.Subvolume.RectangleTiling.index_near line 57
  4. theorem OAI.PolynomialPEPS.Subvolume.RectangleTiling.mod_near_unique line 71
  5. abbrev OAI.PolynomialPEPS.Subvolume.RectangleTiling.Index line 91
  6. def OAI.PolynomialPEPS.Subvolume.RectangleTiling.tile line 93
  7. def OAI.PolynomialPEPS.Subvolume.RectangleTiling.collar line 97
  8. def OAI.PolynomialPEPS.Subvolume.RectangleTiling.box line 101
  9. lemma OAI.PolynomialPEPS.Subvolume.RectangleTiling.mem_tile line 104
  10. lemma OAI.PolynomialPEPS.Subvolume.RectangleTiling.mem_collar line 111
  11. lemma OAI.PolynomialPEPS.Subvolume.RectangleTiling.mem_box line 120
  12. lemma OAI.PolynomialPEPS.Subvolume.RectangleTiling.tile_subset_box line 127
  13. lemma OAI.PolynomialPEPS.Subvolume.RectangleTiling.tiles_cover line 141
  14. lemma OAI.PolynomialPEPS.Subvolume.RectangleTiling.tiles_disjoint line 152
  15. def OAI.PolynomialPEPS.Subvolume.RectangleTiling.color line 161
  16. def OAI.PolynomialPEPS.Subvolume.RectangleTiling.interior line 164
  17. lemma OAI.PolynomialPEPS.Subvolume.RectangleTiling.collar_subset_box line 167
  18. lemma OAI.PolynomialPEPS.Subvolume.RectangleTiling.same_color_disjoint_collar line 188
  19. lemma OAI.PolynomialPEPS.Subvolume.RectangleTiling.collar_exposed line 202
  20. theorem OAI.PolynomialPEPS.Subvolume.RectangleTiling.interior_card_lower line 225
  21. theorem OAI.PolynomialPEPS.Subvolume.RectangleTiling.interior_card_upper line 246