OAI/Geometry/PeriodicTiling/ConstituentGeometry.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PeriodicTilingThree.MarkedTile.castLattice_scale line 13
  2. def OAI.PeriodicTilingThree.MarkedTile.center line 18
  3. theorem OAI.PeriodicTilingThree.MarkedTile.center_zero line 21
  4. def OAI.PeriodicTilingThree.MarkedTile.centers line 24
  5. theorem OAI.PeriodicTilingThree.MarkedTile.mem_centers line 27
  6. theorem OAI.PeriodicTilingThree.MarkedTile.subset_centers line 35
  7. def OAI.PeriodicTilingThree.MarkedTile.ResidueSection.constituent line 44
  8. def OAI.PeriodicTilingThree.MarkedTile.ResidueSection.part line 47
  9. theorem OAI.PeriodicTilingThree.MarkedTile.ResidueSection.mem_part line 50
  10. theorem OAI.PeriodicTilingThree.MarkedTile.ResidueSection.part_subset_finalTile line 65
  11. theorem OAI.PeriodicTilingThree.MarkedTile.ResidueSection.parts_disjoint line 71
  12. theorem OAI.PeriodicTilingThree.MarkedTile.ResidueSection.mem_thickening_part line 81
  13. theorem OAI.PeriodicTilingThree.MarkedTile.ResidueSection.mem_translated_part line 94
  14. theorem OAI.PeriodicTilingThree.MarkedTile.ResidueSection.mem_thickening_finalTile line 100
  15. theorem OAI.PeriodicTilingThree.MarkedTile.ResidueSection.mem_translated_finalTile line 111
  16. theorem OAI.PeriodicTilingThree.MarkedTile.ResidueSection.Tstar_subset_constituent line 118
  17. theorem OAI.PeriodicTilingThree.MarkedTile.ResidueSection.Tstar_nonempty line 127
  18. theorem OAI.PeriodicTilingThree.MarkedTile.ResidueSection.common_voxel_subset_constituent line 133