OAI/Computability/WitnessedChoice/GridGeometry.lean

GitHub source file

116 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WitnessedSeparation.Grid.facePlane line 14
  2. def OAI.WitnessedSeparation.Grid.faceSide line 19
  3. def OAI.WitnessedSeparation.Grid.sideAxis line 24
  4. lemma OAI.WitnessedSeparation.Grid.faceSide_axis line 27
  5. lemma OAI.WitnessedSeparation.Grid.faceSide_injective line 32
  6. lemma OAI.WitnessedSeparation.Grid.support_cycle line 40
  7. lemma OAI.WitnessedSeparation.Grid.edgeFaces_card_le_four line 54
  8. def OAI.WitnessedSeparation.Grid.faceCorner line 74
  9. lemma OAI.WitnessedSeparation.Grid.faceCorner_injective line 82
  10. lemma OAI.WitnessedSeparation.Grid.faceSide_endpoints line 90
  11. abbrev OAI.WitnessedSeparation.Grid.VertexFaces line 101
  12. lemma OAI.WitnessedSeparation.Grid.vertexFaces_card_le_twelve line 104
  13. lemma OAI.WitnessedSeparation.Grid.localGroup_card_le_upper line 120
  14. lemma OAI.WitnessedSeparation.Grid.exists_incident line 129
  15. lemma OAI.WitnessedSeparation.Grid.epsilon_ne_zero line 141
  16. def OAI.WitnessedSeparation.Grid.Configuration.faceValue line 150
  17. lemma OAI.WitnessedSeparation.Grid.Configuration.faceValue_eq line 153
  18. def OAI.WitnessedSeparation.Grid.Configuration.code line 158
  19. lemma OAI.WitnessedSeparation.Grid.Configuration.code_injective line 162
  20. lemma OAI.WitnessedSeparation.Grid.configuration_card_le_upper line 193
  21. structure OAI.WitnessedSeparation.Grid.ParentEdges line 232
  22. def OAI.WitnessedSeparation.Grid.ParentEdges.treeEdges line 242
  23. def OAI.WitnessedSeparation.Grid.ParentEdges.sign line 245
  24. lemma OAI.WitnessedSeparation.Grid.ParentEdges.edge_mem line 248
  25. def OAI.WitnessedSeparation.Grid.ParentEdges.route line 251
  26. lemma OAI.WitnessedSeparation.Grid.ParentEdges.boundary_single line 257
  27. lemma OAI.WitnessedSeparation.Grid.ParentEdges.boundary_parent line 262
  28. lemma OAI.WitnessedSeparation.Grid.ParentEdges.boundary_route line 277
  29. lemma OAI.WitnessedSeparation.Grid.ParentEdges.route_zero_off_tree line 288
  30. def OAI.WitnessedSeparation.Grid.ParentEdges.fundamental line 298
  31. lemma OAI.WitnessedSeparation.Grid.ParentEdges.boundary_fundamental line 301
  32. def OAI.WitnessedSeparation.Grid.ParentEdges.flow line 307
  33. lemma OAI.WitnessedSeparation.Grid.ParentEdges.flow_self line 309
  34. lemma OAI.WitnessedSeparation.Grid.ParentEdges.flow_other line 312
  35. def OAI.WitnessedSeparation.Grid.ParentEdges.solve line 316
  36. lemma OAI.WitnessedSeparation.Grid.ParentEdges.boundary_solve line 318
  37. lemma OAI.WitnessedSeparation.Grid.ParentEdges.solve_zero_off_tree line 325
  38. lemma OAI.WitnessedSeparation.Grid.ParentEdges.extend_scalars line 329
  39. def OAI.WitnessedSeparation.Grid.ConsistentSelection line 355
  40. def OAI.WitnessedSeparation.Grid.selectedVectors line 360
  41. def OAI.WitnessedSeparation.Grid.selectedScalars line 364
  42. lemma OAI.WitnessedSeparation.Grid.selectedVectors_preserves line 367
  43. lemma OAI.WitnessedSeparation.Grid.selectedScalars_preserves line 374
  44. def OAI.WitnessedSeparation.Grid.globalStates line 380
  45. lemma OAI.WitnessedSeparation.Grid.globalStates_compatible line 383
  46. lemma OAI.WitnessedSeparation.Grid.globalStates_charge line 388
  47. def OAI.WitnessedSeparation.Grid.globalConfiguration line 392
  48. theorem OAI.WitnessedSeparation.Grid.extend_consistent_selection line 398
  49. theorem OAI.WitnessedSeparation.Grid.total_charge_of_global_configurations line 414
  50. lemma OAI.WitnessedSeparation.Grid.incident_on_axis line 439
  51. lemma OAI.WitnessedSeparation.Grid.fin_three_other line 474
  52. lemma OAI.WitnessedSeparation.Grid.other_incident line 481
  53. def OAI.WitnessedSeparation.Grid.extendVertexScalars line 493
  54. lemma OAI.WitnessedSeparation.Grid.extendVertexScalars_charge line 499
  55. lemma OAI.WitnessedSeparation.Grid.exists_configuration_two line 510
  56. def OAI.WitnessedSeparation.Grid.vertexCoord line 552
  57. def OAI.WitnessedSeparation.Grid.planeAxis line 554
  58. instance OAI.WitnessedSeparation.Grid.(instance at line 556) line 556
  59. def OAI.WitnessedSeparation.Grid.faceBase line 558
  60. lemma OAI.WitnessedSeparation.Grid.vertexCoord_injective line 560
  61. lemma OAI.WitnessedSeparation.Grid.faceBase_injective line 564
  62. lemma OAI.WitnessedSeparation.Grid.two_axes_plane line 568
  63. lemma OAI.WitnessedSeparation.Grid.plane_axis_exhaust line 573
  64. lemma OAI.WitnessedSeparation.Grid.side_axis_in_plane line 578
  65. lemma OAI.WitnessedSeparation.Grid.faceBase_on_axis line 581
  66. lemma OAI.WitnessedSeparation.Grid.faceBase_outside line 586
  67. lemma OAI.WitnessedSeparation.Grid.common_face_unique line 595
  68. lemma OAI.WitnessedSeparation.Grid.castSucc_ne_succ_self line 634
  69. lemma OAI.WitnessedSeparation.Grid.succ_ne_castSucc_self line 640
  70. lemma OAI.WitnessedSeparation.Grid.cycle_faceSide line 643
  71. lemma OAI.WitnessedSeparation.Grid.faceSide_injective_index line 647
  72. def OAI.WitnessedSeparation.Grid.AdjacentIndex line 652
  73. lemma OAI.WitnessedSeparation.Grid.adjacent_axis_ne line 654
  74. lemma OAI.WitnessedSeparation.Grid.adjacent_common_vertex line 662
  75. def OAI.WitnessedSeparation.Grid.SideAdjacent line 674
  76. lemma OAI.WitnessedSeparation.Grid.sideAdjacent_iff line 679
  77. def OAI.WitnessedSeparation.Grid.SideMatch line 699
  78. lemma OAI.WitnessedSeparation.Grid.index_next_adjacent line 705
  79. lemma OAI.WitnessedSeparation.Grid.nonadjacent_next line 707
  80. lemma OAI.WitnessedSeparation.Grid.sideMatch_iff line 712
  81. def OAI.WitnessedSeparation.Grid.actionPerm line 739
  82. lemma OAI.WitnessedSeparation.Grid.actionPerm_apply line 741
  83. lemma OAI.WitnessedSeparation.Grid.actionPerm_fullAut line 743
  84. def OAI.WitnessedSeparation.Grid.edgeFootprint line 748
  85. def OAI.WitnessedSeparation.Grid.vertexFootprint line 751
  86. lemma OAI.WitnessedSeparation.Grid.edgeFootprint_card line 754
  87. lemma OAI.WitnessedSeparation.Grid.vertexFootprint_card line 760
  88. lemma OAI.WitnessedSeparation.Grid.mem_edgeFootprint line 766
  89. lemma OAI.WitnessedSeparation.Grid.mem_vertexFootprint line 771
  90. def OAI.WitnessedSeparation.Grid.edgeBlockSet line 777
  91. def OAI.WitnessedSeparation.Grid.vertexBlockSet line 780
  92. def OAI.WitnessedSeparation.Grid.affectedAtoms line 783
  93. lemma OAI.WitnessedSeparation.Grid.affectedAtoms_card_le line 786
  94. lemma OAI.WitnessedSeparation.Grid.faceTranslation_moved_subset line 801
  95. lemma OAI.WitnessedSeparation.Grid.faceTranslation_in_localPool_bound line 840
  96. lemma OAI.WitnessedSeparation.Grid.faceTranslation_in_localPool line 855
  97. def OAI.WitnessedSeparation.Grid.AcceptsFaces line 873
  98. def OAI.WitnessedSeparation.Grid.faceDelta line 877
  99. lemma OAI.WitnessedSeparation.Grid.faceDelta_support line 880
  100. lemma OAI.WitnessedSeparation.Grid.faceDelta_zero_on_past line 886
  101. lemma OAI.WitnessedSeparation.Grid.faceDelta_fix_past line 894
  102. lemma OAI.WitnessedSeparation.Grid.faceDelta_hits_vectors line 906
  103. lemma OAI.WitnessedSeparation.Grid.faceDelta_in_localPool line 912
  104. lemma OAI.WitnessedSeparation.Grid.central_after_local line 919
  105. lemma OAI.WitnessedSeparation.Grid.central_fix_edge line 936
  106. lemma OAI.WitnessedSeparation.Grid.path_walk_lower line 957
  107. lemma OAI.WitnessedSeparation.Grid.path_walk_upper_le line 967
  108. lemma OAI.WitnessedSeparation.Grid.path_dist line 982
  109. lemma OAI.WitnessedSeparation.Grid.path_edist line 996
  110. def OAI.WitnessedSeparation.Grid.boxGraph line 999
  111. lemma OAI.WitnessedSeparation.Grid.boxGraph_connected line 1002
  112. lemma OAI.WitnessedSeparation.Grid.boxGraph_dist line 1005
  113. lemma OAI.WitnessedSeparation.Grid.boxGraph_tail_head line 1011
  114. lemma OAI.WitnessedSeparation.Grid.boxGraph_adj_iff line 1015
  115. def OAI.WitnessedSeparation.Grid.cornerAnchors line 1061
  116. lemma OAI.WitnessedSeparation.Grid.cornerAnchors_resolve line 1064