OAI/SetTheory/PartitionPrinciple/Geometry/GroundCompressionStarIncidence.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.externalCosetRelation line 11
  2. theorem OAI.PartitionPilot.Forcing.externalCosetRelation_subset line 16
  3. theorem OAI.PartitionPilot.Forcing.pair_mem_externalCosetRelation line 20
  4. def OAI.PartitionPilot.Forcing.BoundedFormula.externalCosetEntryFormula line 34
  5. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_externalCosetEntryFormula line 40
  6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalCosetRelation_mem line 55
  7. theorem OAI.PartitionPilot.Forcing.externalCosetRelation_iff line 94
  8. theorem OAI.PartitionPilot.Forcing.externalCosetRelation_equivalence line 109
  9. theorem OAI.PartitionPilot.Forcing.externalCosetRelation_related line 130
  10. def OAI.PartitionPilot.Forcing.externalCosetPresentation line 135
  11. theorem OAI.PartitionPilot.Forcing.externalCosetPresentation_carrier line 140
  12. theorem OAI.PartitionPilot.Forcing.externalCosetPresentation_encode_point line 144
  13. theorem OAI.PartitionPilot.Forcing.externalCosetClassifier_entry_iff line 148
  14. theorem OAI.PartitionPilot.Forcing.externalCosetClassifier_eq_graph line 156
  15. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalFamilyGroupPresentation line 183
  16. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalFamilyGroupPresentation_carrier line 190
  17. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalFamilyGroupPresentation_multiplication line 200
  18. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalFamilyGroupPresentation_old line 211
  19. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalFamilyGroupPresentation_generators line 222
  20. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalFamilyGroupPresentation_identity line 234
  21. structure OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs line 252
  22. theorem OAI.PartitionPilot.Forcing.GroundCompressionOrigin.externalGeometryInputs line 276
  23. def OAI.PartitionPilot.Forcing.TransitiveGround.externalCosetEquivalence line 306
  24. def OAI.PartitionPilot.Forcing.TransitiveGround.externalCosetCarrier line 309
  25. def OAI.PartitionPilot.Forcing.TransitiveGround.externalCosetClassifier line 311
  26. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalCoset_old_entries line 331
  27. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalCoset_mul_entries line 341
  28. def OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalCosetPresentation line 351
  29. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalCosetPresentation_carrier line 359
  30. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalCosetEquivalence_iff line 369
  31. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalCosetClassifier_entry_iff line 380
  32. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalCosetClassifier_graph line 393
  33. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalCosets_ground line 406
  34. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalCosets_spec line 415
  35. def OAI.PartitionPilot.Forcing.TransitiveGround.externalStarVertices line 438
  36. def OAI.PartitionPilot.Forcing.TransitiveGround.externalStarEdges line 440
  37. def OAI.PartitionPilot.Forcing.TransitiveGround.externalStarDarts line 442
  38. def OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalStarVertexPresentation line 467
  39. def OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalStarEdgePresentation line 473
  40. def OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalStarDartPresentation line 479
  41. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalStarPresentations_carriers line 485
  42. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalStarCarriers_ground line 502
  43. def OAI.PartitionPilot.Forcing.tileStarRequestGraph line 519
  44. theorem OAI.PartitionPilot.Forcing.pair_mem_tileStarRequestGraph line 522
  45. theorem OAI.PartitionPilot.Forcing.externalRequestChildCode_mem line 533
  46. theorem OAI.PartitionPilot.Forcing.TransitiveGround.tileStarRequestGraph_mem line 543
  47. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_groundInitialExternalGeometryInputs line 564
  48. def OAI.PartitionPilot.Forcing.TransitiveGround.externalStarSource line 622
  49. def OAI.PartitionPilot.Forcing.TransitiveGround.externalStarTarget line 626
  50. def OAI.PartitionPilot.Forcing.TransitiveGround.externalStarReverse line 630
  51. def OAI.PartitionPilot.Forcing.TransitiveGround.externalStarIncidence line 632
  52. def OAI.PartitionPilot.Forcing.TransitiveGround.externalStarAdjacency line 634
  53. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalStar_request_entries line 662
  54. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalStar_generator_entries line 674
  55. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalStarSource_iff line 684
  56. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalStarTarget_iff line 701
  57. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalStarReverse_iff line 718
  58. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalStarIncidence_iff line 729
  59. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalStarAdjacency_iff line 746
  60. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalStarEndpoint_functions line 764
  61. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalStarIncidence_ground line 782