OAI/SetTheory/PartitionPrinciple/Geometry/PrincipalBatch.lean

GitHub source file

150 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.Same line 14
  2. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.cosetSetoid line 16
  3. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.Vertex line 27
  4. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.point line 28
  5. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.root line 30
  6. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.point_eq line 32
  7. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.root_eq_point line 35
  8. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.act line 39
  9. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.act_point line 44
  10. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.act_root line 46
  11. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.act_one line 50
  12. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.act_mul line 54
  13. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.Dart line 59
  14. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.reverse line 61
  15. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.startRep line 63
  16. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.endRep line 66
  17. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.letter line 69
  18. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.source line 70
  19. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.target line 71
  20. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.signed_true line 73
  21. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.signed_false line 75
  22. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.end_eq line 79
  23. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.reverse_reverse line 86
  24. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.source_reverse line 90
  25. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.target_reverse line 94
  26. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.cancellation_reverses_edge line 98
  27. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.translate line 118
  28. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.source_translate line 120
  29. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.target_translate line 127
  30. inductive OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.Follows line 134
  31. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.follows_cons_source line 139
  32. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.follows_tail line 144
  33. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.follows_append line 149
  34. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.follows_translate line 156
  35. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.NoBacktracking line 173
  36. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.follows_empty_eq line 178
  37. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.follows_singleton_target line 184
  38. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.path_word line 189
  39. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.no_closed_reduced_path line 223
  40. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.Reachable line 242
  41. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.reachable_one line 245
  42. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.reachable_old line 247
  43. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.reachable_mul line 253
  44. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.reachable_generator line 261
  45. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.reachable_generator_inv line 268
  46. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.reachable_free line 276
  47. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.reachable_element line 285
  48. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.connected line 294
  49. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.IsIndexedTree line 298
  50. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.coset_tree line 302
  51. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.reversal_of_not_reduced line 305
  52. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.closed_path_has_reversal line 319
  53. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.groupOfData line 325
  54. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.taskSystem_coset_tree line 334
  55. def OAI.PartitionPilot.Compression.RecursiveMaps.EdgeWords.reverse line 351
  56. def OAI.PartitionPilot.Compression.RecursiveMaps.EdgeWords.NoBacktracking line 353
  57. theorem OAI.PartitionPilot.Compression.RecursiveMaps.EdgeWords.mk_cons line 358
  58. theorem OAI.PartitionPilot.Compression.RecursiveMaps.EdgeWords.mk_reverse line 362
  59. theorem OAI.PartitionPilot.Compression.RecursiveMaps.EdgeWords.mk_delete_reversal line 367
  60. theorem OAI.PartitionPilot.Compression.RecursiveMaps.EdgeWords.reduce_of_no_backtracking line 371
  61. theorem OAI.PartitionPilot.Compression.RecursiveMaps.EdgeWords.reduced_word_eq_one_iff line 390
  62. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.follows_delete_reversal line 408
  63. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.closed_edge_word line 423
  64. abbrev OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.Center line 456
  65. abbrev OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.OldEdge line 457
  66. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.Vertex line 458
  67. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.Edge line 459
  68. abbrev OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.Dart line 460
  69. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.reverse line 462
  70. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.centerOf line 466
  71. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.source line 468
  72. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.target line 475
  73. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.reverse_reverse line 478
  74. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.source_reverse line 482
  75. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.target_reverse line 485
  76. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.root line 489
  77. inductive OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.Follows line 491
  78. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.follows_append line 497
  79. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.contract line 504
  80. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.projectDart line 508
  81. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.project line 513
  82. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.contract_edge line 516
  83. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.follows_project line 525
  84. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.expandDart line 533
  85. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.expand_edge line 539
  86. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.follows_expand line 549
  87. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.connected line 556
  88. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.potential line 578
  89. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.expandHom line 582
  90. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.edge_word line 586
  91. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.path_word line 618
  92. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.closed_edge_word line 634
  93. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.no_closed_reduced_path line 642
  94. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.IsIndexedTree line 649
  95. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.tile_star_tree line 653
  96. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.reversal_of_not_reduced line 656
  97. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.closed_path_has_reversal line 670
  98. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.requested_tile_tree line 675
  99. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.taskSystem_tile_tree line 679
  100. theorem OAI.PartitionPilot.Compression.RecursiveMaps.EdgeWords.reduced_words_injective line 696
  101. theorem OAI.PartitionPilot.Compression.RecursiveMaps.EdgeWords.no_backtracking_append_left line 704
  102. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.follows_cons_source line 720
  103. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.follows_tail line 725
  104. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.follows_delete_reversal line 731
  105. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.reduced_path line 747
  106. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.follows_reverse line 769
  107. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.path_words_equal line 782
  108. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.reduced_path_unique line 790
  109. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.unique_root_path line 795
  110. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.rootPath line 801
  111. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.rootPath_follows line 804
  112. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.rootPath_reduced line 808
  113. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.rootPath_eq line 812
  114. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.rootPath_root line 818
  115. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.depth line 821
  116. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.rootPath_shortest line 823
  117. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.follows_empty_eq line 829
  118. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.rootPath_empty_iff line 835
  119. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.follows_last line 843
  120. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.exists_parent_edge line 858
  121. structure OAI.PartitionPilot.Compression.RecursiveMaps.IdealEmbedding line 885
  122. def OAI.PartitionPilot.Compression.RecursiveMaps.IdealEmbedding.identity line 894
  123. def OAI.PartitionPilot.Compression.RecursiveMaps.IdealEmbedding.comp line 898
  124. def OAI.PartitionPilot.Compression.RecursiveMaps.IdealEmbedding.ofOrderMap line 905
  125. theorem OAI.PartitionPilot.Compression.RecursiveMaps.IdealEmbedding.principal line 925
  126. theorem OAI.PartitionPilot.Compression.RecursiveMaps.IdealEmbedding.principal_surjective line 932
  127. def OAI.PartitionPilot.Compression.RecursiveMaps.IdealEmbedding.principalIso line 938
  128. def OAI.PartitionPilot.Compression.RecursiveMaps.IdealEmbedding.projection line 950
  129. theorem OAI.PartitionPilot.Compression.RecursiveMaps.IdealEmbedding.projection_spec line 953
  130. theorem OAI.PartitionPilot.Compression.RecursiveMaps.IdealEmbedding.greatest_part line 957
  131. structure OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family line 977
  132. def OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.Fresh line 986
  133. def OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.Node line 987
  134. def OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.Inside line 989
  135. def OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.data line 992
  136. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.component_meets line 1020
  137. def OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.extension line 1039
  138. def OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.old line 1041
  139. def OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.componentMap line 1048
  140. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.componentMap_le line 1052
  141. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.componentMap_ideal line 1070
  142. def OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.component line 1086
  143. def OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.tile line 1089
  144. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.tile_old_overlap line 1094
  145. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.cover line 1102
  146. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.fresh_old_meet line 1110
  147. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.fresh_greatest_old_part line 1115
  148. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.different_fresh_incomparable line 1118
  149. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.old_vertex_preserved line 1125
  150. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.tile_vertex_preserved line 1129