OAI/SetTheory/PartitionPrinciple/Geometry/ExternalTranslation.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.fullIdeal line 15
  2. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.vertexIdealIso line 23
  3. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.Space line 27
  4. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.localOrder line 31
  5. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.leftAnchor line 35
  6. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.rightAnchor line 41
  7. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.edgeOverlap line 47
  8. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.diagram line 58
  9. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.Node line 65
  10. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.gluedOrder line 66
  11. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.copy line 68
  12. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.placedTile line 71
  13. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.copy_coordinate line 74
  14. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.copy_one line 81
  15. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.stem_formula line 86
  16. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.branch_formula line 92
  17. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.root_identification line 102
  18. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.child_identification line 111
  19. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.copy_principal line 123
  20. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.copy_greatest_part line 127
  21. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.copy_cover line 132
  22. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.comparison_in_copy line 147
  23. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.copy_injective line 153
  24. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.transfer_child_root line 172
  25. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.transfer_child_root_meet line 177
  26. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.transfer_child_child_meet line 185
  27. abbrev OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.AllGeometry.family line 200
  28. abbrev OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.AllGeometry.Letters line 201
  29. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.AllGeometry.separation_fixes line 203
  30. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.AllGeometry.separation_meet line 210
  31. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.AllGeometry.compression_restriction line 219
  32. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.AllGeometry.compression_top line 227
  33. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.AllGeometry.rectangle_first_agrees line 235
  34. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.AllGeometry.rectangle_second_agrees line 243
  35. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.AllGeometry.rectangle_children_intersection line 251
  36. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.AllGeometry.rectangle_first_meet_root line 267
  37. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.AllGeometry.rectangle_second_meet_root line 277
  38. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.AllGeometry.rectangle_children_meet line 287
  39. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.Spaces.values_respect_parents line 312
  40. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.Spaces.descend line 320
  41. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.Spaces.descend_vertex line 324
  42. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.Spaces.descend_unique line 330
  43. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.translationValue line 347
  44. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.translationValue_copy line 352
  45. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.translation_stem line 359
  46. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.translation_branch line 369
  47. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.translation_edges line 382
  48. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.translate line 393
  49. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.translate_vertex line 396
  50. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.translate_copy line 401
  51. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.translate_tile line 407