OAI/Computability/WitnessedChoice/AnchoredTree.lean

GitHub source file

93 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WitnessedChoice.AnchoredTree.key line 16
  2. def OAI.WitnessedChoice.AnchoredTree.Resolving line 19
  3. def OAI.WitnessedChoice.AnchoredTree.Eligible line 21
  4. lemma OAI.WitnessedChoice.AnchoredTree.root_lt line 24
  5. lemma OAI.WitnessedChoice.AnchoredTree.least_iff_root line 33
  6. lemma OAI.WitnessedChoice.AnchoredTree.exists_eligible line 43
  7. lemma OAI.WitnessedChoice.AnchoredTree.exists_min_key line 58
  8. lemma OAI.WitnessedChoice.AnchoredTree.exists_parent line 69
  9. def OAI.WitnessedChoice.AnchoredTree.parent line 77
  10. lemma OAI.WitnessedChoice.AnchoredTree.parent_property line 80
  11. def OAI.WitnessedChoice.AnchoredTree.rooted line 87
  12. lemma OAI.WitnessedChoice.AnchoredTree.parent_iff line 93
  13. lemma OAI.WitnessedChoice.BGS.QuotedFormula.meaning_vertexLt line 125
  14. lemma OAI.WitnessedChoice.BGS.QuotedFormula.meaning_resolving line 153
  15. lemma OAI.WitnessedSeparation.Grid.configuration_exists line 198
  16. lemma OAI.WitnessedSeparation.Grid.mem_edgeBlockSet line 204
  17. lemma OAI.WitnessedSeparation.Grid.mem_vertexBlockSet line 209
  18. lemma OAI.WitnessedSeparation.Grid.edgeBlockSet_injective line 214
  19. lemma OAI.WitnessedSeparation.Grid.vertexBlockSet_injective line 221
  20. lemma OAI.WitnessedSeparation.Grid.edgeRow_grid line 229
  21. lemma OAI.WitnessedSeparation.Grid.vertexRow_grid line 240
  22. lemma OAI.WitnessedSeparation.Grid.edgeBlocks_grid line 251
  23. lemma OAI.WitnessedSeparation.Grid.vertexBlocks_grid line 262
  24. def OAI.WitnessedSeparation.Grid.vertexCode line 274
  25. def OAI.WitnessedSeparation.Grid.edgeCode line 276
  26. lemma OAI.WitnessedSeparation.Grid.vertexCode_injective line 278
  27. lemma OAI.WitnessedSeparation.Grid.edgeCode_injective line 281
  28. lemma OAI.WitnessedSeparation.Grid.blockIncident_grid line 284
  29. def OAI.WitnessedSeparation.Grid.edgeGraph line 311
  30. lemma OAI.WitnessedSeparation.Grid.edgeGraph_univ line 319
  31. lemma OAI.WitnessedSeparation.Grid.blockAdjacent_edges line 323
  32. lemma OAI.WitnessedSeparation.Grid.vertex_card_le_atoms line 340
  33. lemma OAI.WitnessedSeparation.Grid.quoted_vertexBlocks line 346
  34. lemma OAI.WitnessedSeparation.Grid.quoted_edgeBlocks line 352
  35. lemma OAI.WitnessedSeparation.Grid.xy_incident_face line 370
  36. lemma OAI.WitnessedSeparation.Grid.xz_incident_face line 385
  37. lemma OAI.WitnessedSeparation.Grid.yz_incident_face line 400
  38. lemma OAI.WitnessedSeparation.Grid.incident_perpendicular_face line 415
  39. lemma OAI.WitnessedSeparation.Grid.square_common_neighbors line 444
  40. abbrev OAI.WitnessedSeparation.Grid.Direction line 463
  41. def OAI.WitnessedSeparation.Grid.directionVector line 465
  42. def OAI.WitnessedSeparation.Grid.oppositeDirection line 468
  43. lemma OAI.WitnessedSeparation.Grid.direction_neg line 470
  44. lemma OAI.WitnessedSeparation.Grid.four_direction_pattern line 475
  45. def OAI.WitnessedSeparation.Grid.vertexInt line 494
  46. lemma OAI.WitnessedSeparation.Grid.vertexInt_injective line 496
  47. lemma OAI.WitnessedSeparation.Grid.head_vertexInt line 503
  48. lemma OAI.WitnessedSeparation.Grid.endpoints_direction line 510
  49. lemma OAI.WitnessedSeparation.Grid.square_consecutive_perpendicular line 521
  50. lemma OAI.WitnessedSeparation.Grid.faceCorner_index_injective line 561
  51. lemma OAI.WitnessedSeparation.Grid.incident_faceSide line 566
  52. lemma OAI.WitnessedSeparation.Grid.square_index_calculation line 571
  53. lemma OAI.WitnessedSeparation.Grid.face_chain_opposite line 575
  54. lemma OAI.WitnessedSeparation.Grid.edge_eq_of_endpoints line 597
  55. def OAI.WitnessedSeparation.Grid.symEdge line 616
  56. lemma OAI.WitnessedSeparation.Grid.symEdge_injective line 618
  57. lemma OAI.WitnessedSeparation.Grid.edgeGraph_edgeFinset line 623
  58. lemma OAI.WitnessedSeparation.Grid.edgeGraph_card line 640
  59. lemma OAI.WitnessedSeparation.Grid.ParentEdges.edge_injective line 649
  60. lemma OAI.WitnessedSeparation.Grid.ParentEdges.graph_adj line 675
  61. lemma OAI.WitnessedSeparation.Grid.ParentEdges.graph_reachable_root line 698
  62. lemma OAI.WitnessedSeparation.Grid.ParentEdges.graph_connected line 706
  63. lemma OAI.WitnessedSeparation.Grid.ParentEdges.card_treeEdges line 710
  64. lemma OAI.WitnessedSeparation.Grid.ParentEdges.graph_isTree line 719
  65. lemma OAI.WitnessedChoice.BGS.QuotedFormula.meaning_leastVertex line 742
  66. lemma OAI.WitnessedChoice.BGS.QuotedTerm.meaning_root line 765
  67. def OAI.WitnessedSeparation.Grid.anchoredTree line 806
  68. def OAI.WitnessedSeparation.Grid.anchoredParents line 809
  69. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.meaning_incident line 825
  70. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.meaning_adjacent line 832
  71. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.meaning_parentEligible line 841
  72. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.meaning_parent line 859
  73. lemma OAI.WitnessedSeparation.Grid.endpoints_iff_incident line 903
  74. lemma OAI.WitnessedSeparation.Grid.edge_eq_of_common_incidents line 917
  75. lemma OAI.WitnessedSeparation.Grid.edge_on_face line 929
  76. lemma OAI.WitnessedSeparation.Grid.indexed_cycle_incident line 953
  77. theorem OAI.WitnessedSeparation.Grid.indexed_fourcycle_is_face line 961
  78. structure OAI.WitnessedSeparation.Grid.CycleFrame line 1018
  79. def OAI.WitnessedSeparation.Grid.CycleFrame.face line 1030
  80. lemma OAI.WitnessedSeparation.Grid.CycleFrame.on_face line 1032
  81. lemma OAI.WitnessedSeparation.Grid.CycleFrame.incident_ends line 1035
  82. lemma OAI.WitnessedSeparation.Grid.CycleFrame.consecutive_axis_ne line 1038
  83. lemma OAI.WitnessedSeparation.Grid.CycleFrame.adjacent_axis_ne line 1046
  84. lemma OAI.WitnessedSeparation.Grid.CycleFrame.support_iff line 1051
  85. lemma OAI.WitnessedSeparation.Grid.CycleFrame.face_unique line 1065
  86. def OAI.WitnessedSeparation.Grid.CycleFrame.joint line 1069
  87. lemma OAI.WitnessedSeparation.Grid.CycleFrame.joint_incident line 1071
  88. def OAI.WitnessedSeparation.Grid.CycleFrame.Across line 1081
  89. lemma OAI.WitnessedSeparation.Grid.CycleFrame.across_iff line 1085
  90. def OAI.WitnessedSeparation.Grid.CycleFrame.Match line 1103
  91. lemma OAI.WitnessedSeparation.Grid.CycleFrame.match_iff line 1107
  92. def OAI.WitnessedSeparation.Grid.standardFrame line 1122
  93. lemma OAI.WitnessedSeparation.Grid.standardFrame_face line 1141