OAI/SetTheory/PartitionPrinciple/Geometry/GluingHeights.lean

GitHub source file

97 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.representative_exists line 14
  2. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.representative line 18
  3. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.representative_spec line 22
  4. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.representative_root line 31
  5. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.coordinate_exists line 34
  6. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.coordinate line 38
  7. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.coordinate_spec line 40
  8. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.coordinate_unique line 44
  9. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.point_mul_old line 48
  10. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.coordinate_mul_old line 51
  11. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.coordinate_one line 56
  12. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.coordinate_old line 61
  13. structure OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.OrderAction line 65
  14. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.OrderAction.chart line 73
  15. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.OrderAction.chart_one line 75
  16. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.OrderAction.chart_mul_old line 79
  17. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.OrderAction.Label line 85
  18. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.OrderAction.label line 87
  19. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.OrderAction.label_mul_old line 90
  20. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.OrderAction.label_same_rep line 96
  21. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.OrderAction.label_eq_iff line 103
  22. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.OrderAction.ideal line 114
  23. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.OrderAction.fixes_top line 118
  24. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.taskSystem_orderAction line 126
  25. structure OAI.PartitionPilot.SetRealization.GeometryPresentation line 142
  26. def OAI.PartitionPilot.SetRealization.GeometryPresentation.orderRelation line 150
  27. def OAI.PartitionPilot.SetRealization.GeometryPresentation.meetGraph line 153
  28. def OAI.PartitionPilot.SetRealization.GeometryPresentation.multiplicationGraph line 156
  29. def OAI.PartitionPilot.SetRealization.GeometryPresentation.inverseGraph line 159
  30. def OAI.PartitionPilot.SetRealization.GeometryPresentation.actionGraph line 162
  31. def OAI.PartitionPilot.SetRealization.GeometryPresentation.package line 165
  32. theorem OAI.PartitionPilot.SetRealization.GeometryPresentation.orderRelation_iff line 172
  33. theorem OAI.PartitionPilot.SetRealization.GeometryPresentation.meetGraph_iff line 177
  34. theorem OAI.PartitionPilot.SetRealization.GeometryPresentation.multiplicationGraph_iff line 182
  35. theorem OAI.PartitionPilot.SetRealization.GeometryPresentation.inverseGraph_iff line 187
  36. theorem OAI.PartitionPilot.SetRealization.GeometryPresentation.actionGraph_iff line 191
  37. theorem OAI.PartitionPilot.SetRealization.GeometryPresentation.operation_graphs_are_functions line 196
  38. structure OAI.PartitionPilot.SetRealization.GeometryPresentation.RankBounds line 206
  39. theorem OAI.PartitionPilot.SetRealization.GeometryPresentation.rank_bounds line 218
  40. structure OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Tile line 256
  41. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Tile.binary line 266
  42. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Tile.rectangle line 276
  43. inductive OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Request line 292
  44. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Request.Child line 300
  45. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Request.tile line 305
  46. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Request.separation_agrees line 310
  47. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Request.compression_agrees line 315
  48. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Request.rectangle_agrees line 321
  49. structure OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family line 331
  50. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.Child line 339
  51. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.Letters line 340
  52. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.tile line 341
  53. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.all line 343
  54. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.Spaces.Realizes line 359
  55. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.Spaces.realizes_reindex line 363
  56. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.Spaces.Equation line 370
  57. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.Spaces.equation_of_reverse line 376
  58. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.Spaces.incoming_realizes line 398
  59. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.Spaces.equation_of_extension line 406
  60. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.Spaces.equations_of_parents line 419
  61. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.Spaces.edge_identification line 428
  62. theorem OAI.PartitionPilot.Compression.RecursiveMaps.IdealEmbedding.projection_mono line 449
  63. theorem OAI.PartitionPilot.Compression.RecursiveMaps.IdealEmbedding.projection_image line 455
  64. theorem OAI.PartitionPilot.Compression.RecursiveMaps.IdealEmbedding.projected_strict line 462
  65. theorem OAI.PartitionPilot.Compression.RecursiveMaps.LinearHeightOrder.lex_weak line 477
  66. theorem OAI.PartitionPilot.Compression.RecursiveMaps.LinearHeightOrder.lex_strict line 485
  67. theorem OAI.PartitionPilot.Compression.RecursiveMaps.countable_range_pair line 496
  68. theorem OAI.PartitionPilot.Compression.RecursiveMaps.countable_range_precompose line 504
  69. def OAI.PartitionPilot.Compression.RecursiveMaps.RationalHeights.zero line 511
  70. def OAI.PartitionPilot.Compression.RecursiveMaps.RationalHeights.one line 512
  71. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RationalHeights.zero_lt_one line 514
  72. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RationalHeights.rational_assignment line 518
  73. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Tile.binaryTuple line 534
  74. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Tile.rectangleTuple line 545
  75. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Tile.binaryTuple_countable line 563
  76. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Tile.rectangleTuple_countable line 568
  77. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Tile.binaryHeight line 575
  78. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Tile.rectangleHeight line 580
  79. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Request.rationalHeight line 593
  80. def OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.heightValue line 615
  81. def OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.extendHeight line 619
  82. structure OAI.PartitionPilot.Compression.RecursiveMaps.IdealChain.HeightSystem line 649
  83. theorem OAI.PartitionPilot.Compression.RecursiveMaps.IdealChain.HeightSystem.up line 656
  84. def OAI.PartitionPilot.Compression.RecursiveMaps.IdealChain.HeightSystem.value line 662
  85. theorem OAI.PartitionPilot.Compression.RecursiveMaps.IdealChain.HeightSystem.value_point line 667
  86. def OAI.PartitionPilot.Compression.RecursiveMaps.IdealChain.HeightSystem.unionHeight line 670
  87. theorem OAI.PartitionPilot.Compression.RecursiveMaps.IdealChain.HeightSystem.unionHeight_countable line 677
  88. structure OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.BoundedHeight line 709
  89. def OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.nextBounded line 713
  90. def OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.boundedStages line 727
  91. def OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.heightSystem line 731
  92. def OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.externalHeight line 735
  93. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.externalHeight_stage line 738
  94. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.externalHeight_original line 742
  95. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.boundedStages_countable line 748
  96. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.externalHeight_countable line 777
  97. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.externalHeight_column_bound line 782