OAI/Geometry/PeriodicTiling/MarkedTile.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PeriodicTilingThree.MarkedTile.Residue line 12
  2. def OAI.PeriodicTilingThree.MarkedTile.scale line 14
  3. theorem OAI.PeriodicTilingThree.MarkedTile.scale_apply line 19
  4. theorem OAI.PeriodicTilingThree.MarkedTile.scale_injective line 22
  5. def OAI.PeriodicTilingThree.MarkedTile.residue line 28
  6. theorem OAI.PeriodicTilingThree.MarkedTile.residue_apply line 33
  7. theorem OAI.PeriodicTilingThree.MarkedTile.residue_scale line 36
  8. theorem OAI.PeriodicTilingThree.MarkedTile.exists_scale_of_residue_eq_zero line 41
  9. structure OAI.PeriodicTilingThree.MarkedTile.ResidueSection line 50
  10. theorem OAI.PeriodicTilingThree.MarkedTile.ResidueSection.residue_t_apply line 58
  11. theorem OAI.PeriodicTilingThree.MarkedTile.ResidueSection.t_injective line 61
  12. def OAI.PeriodicTilingThree.MarkedTile.ResidueSection.t0 line 66
  13. theorem OAI.PeriodicTilingThree.MarkedTile.ResidueSection.residue_t0 line 68
  14. theorem OAI.PeriodicTilingThree.MarkedTile.ResidueSection.coordinates_injective line 70
  15. theorem OAI.PeriodicTilingThree.MarkedTile.ResidueSection.coordinates_surjective line 80
  16. theorem OAI.PeriodicTilingThree.MarkedTile.ResidueSection.coordinates_bijective line 89
  17. def OAI.PeriodicTilingThree.MarkedTile.ResidueSection.T0 line 97
  18. def OAI.PeriodicTilingThree.MarkedTile.ResidueSection.Tstar line 99
  19. def OAI.PeriodicTilingThree.MarkedTile.ResidueSection.t1 line 101
  20. def OAI.PeriodicTilingThree.MarkedTile.ResidueSection.T1 line 104
  21. theorem OAI.PeriodicTilingThree.MarkedTile.ResidueSection.mem_T0 line 106
  22. theorem OAI.PeriodicTilingThree.MarkedTile.ResidueSection.t0_mem_T0 line 110
  23. theorem OAI.PeriodicTilingThree.MarkedTile.ResidueSection.mem_Tstar line 113
  24. theorem OAI.PeriodicTilingThree.MarkedTile.ResidueSection.residue_t1 line 130
  25. theorem OAI.PeriodicTilingThree.MarkedTile.ResidueSection.t1_injective line 139
  26. theorem OAI.PeriodicTilingThree.MarkedTile.ResidueSection.mem_T1 line 144
  27. theorem OAI.PeriodicTilingThree.MarkedTile.ResidueSection.T1_eq_insert line 148
  28. theorem OAI.PeriodicTilingThree.MarkedTile.ResidueSection.card_T0 line 165
  29. theorem OAI.PeriodicTilingThree.MarkedTile.ResidueSection.card_Tstar line 170
  30. theorem OAI.PeriodicTilingThree.MarkedTile.ResidueSection.card_T1 line 174
  31. def OAI.PeriodicTilingThree.MarkedTile.ResidueSection.point line 179
  32. theorem OAI.PeriodicTilingThree.MarkedTile.ResidueSection.point_zero line 182
  33. theorem OAI.PeriodicTilingThree.MarkedTile.ResidueSection.point_of_ne_zero line 189
  34. theorem OAI.PeriodicTilingThree.MarkedTile.ResidueSection.residue_point line 196
  35. theorem OAI.PeriodicTilingThree.MarkedTile.ResidueSection.point_injective line 205
  36. def OAI.PeriodicTilingThree.MarkedTile.ResidueSection.finalTile line 245
  37. theorem OAI.PeriodicTilingThree.MarkedTile.ResidueSection.mem_finalTile line 248
  38. theorem OAI.PeriodicTilingThree.MarkedTile.ResidueSection.card_finalTile line 258
  39. theorem OAI.PeriodicTilingThree.MarkedTile.ResidueSection.finalTile_nonempty line 264
  40. theorem OAI.PeriodicTilingThree.MarkedTile.ResidueSection.finalTile_eq_union line 268
  41. theorem OAI.PeriodicTilingThree.MarkedTile.ResidueSection.constituent_disjoint line 295