OAI/SetTheory/PartitionPrinciple/Geometry/GroundExternalLocalHeightSelection.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.BoundedFormula.intervalHeightCandidateFormula line 15
  2. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_intervalHeightCandidateFormula line 23
  3. def OAI.PartitionPilot.Forcing.BoundedFormula.intervalHeightRelationEntryFormula line 38
  4. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_intervalHeightRelationEntryFormula line 45
  5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.intervalHeightRelation_mem line 70
  6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_intervalHeight_family line 108
  7. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalPointOrder line 164
  8. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalPointMeet line 169
  9. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalPointAction line 172
  10. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalCopyGraph line 178
  11. structure OAI.PartitionPilot.Forcing.GroundExternalGeometryData line 184
  12. def OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalPointPresentation line 229
  13. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalPointPresentation_carrier line 242
  14. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalPointClassifier_entry_iff line 252
  15. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalGeometry_entries line 278
  16. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalGeometryData line 328
  17. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_groundInitialExternalGeometry line 387
  18. def OAI.PartitionPilot.Forcing.vertexImageDomains line 445
  19. theorem OAI.PartitionPilot.Forcing.pair_mem_vertexImageDomains line 450
  20. def OAI.PartitionPilot.Forcing.BoundedFormula.vertexImageDomainsEntryFormula line 465
  21. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_vertexImageDomainsEntryFormula line 471
  22. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.localTileVertexImages line 495
  23. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.localTilePoints line 501
  24. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.localTileCarrier line 504
  25. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.localTileOrder line 507
  26. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.localTileMeet line 512
  27. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.localTileCarriers line 517
  28. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.localTileOrders line 520
  29. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.localTileMeets line 525
  30. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.localTileVertexGraphs line 530
  31. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.localTileCarrier_subset line 534
  32. structure OAI.PartitionPilot.Forcing.GroundExternalLocalHeightData line 546
  33. theorem OAI.PartitionPilot.Forcing.TransitiveGround.vertexImageDomains_mem line 568
  34. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.localTileGroundInputs line 612
  35. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.localTileCarriers_spec line 626
  36. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.localTileOrders_spec line 636
  37. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.localTileMeets_spec line 648
  38. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.localTileVertexGraphs_spec line 660
  39. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.localHeightFamily_of_witnesses line 695