OAI/SetTheory/PartitionPrinciple/Definability/CompressionExternalStepRealization.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.ExternalFlatVertexWordCode line 13
  2. def OAI.PartitionPilot.Forcing.externalFlatPlacements line 19
  3. theorem OAI.PartitionPilot.Forcing.triple_mem_externalFlatPlacements line 26
  4. def OAI.PartitionPilot.Forcing.BoundedFormula.externalFlatVertexWordFormula line 44
  5. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_externalFlatVertexWordFormula line 53
  6. def OAI.PartitionPilot.Forcing.BoundedFormula.externalFlatPlacementEntryFormula line 62
  7. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_externalFlatPlacementEntryFormula line 76
  8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalFlatPlacements_mem line 93
  9. def OAI.PartitionPilot.Forcing.ExternalFlatCoordinateCode line 134
  10. def OAI.PartitionPilot.Forcing.ExternalFlatTileStepCode line 139
  11. def OAI.PartitionPilot.Forcing.ExternalFlatStepCode line 144
  12. theorem OAI.PartitionPilot.Forcing.ExternalFlatStepCode.symm line 148
  13. def OAI.PartitionPilot.Forcing.externalFlatStepGraph line 152
  14. theorem OAI.PartitionPilot.Forcing.pair_mem_externalFlatStepGraph line 157
  15. theorem OAI.PartitionPilot.Forcing.externalFlatStepGraph_subset line 169
  16. theorem OAI.PartitionPilot.Forcing.externalFlatStepGraph_symmetric line 174
  17. def OAI.PartitionPilot.Forcing.BoundedFormula.externalFlatCoordinateFormula line 182
  18. def OAI.PartitionPilot.Forcing.BoundedFormula.externalFlatTileStepFormula line 191
  19. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_externalFlatCoordinateFormula line 197
  20. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_externalFlatTileStepFormula line 204
  21. def OAI.PartitionPilot.Forcing.BoundedFormula.externalFlatStepFormula line 211
  22. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_externalFlatStepFormula line 215
  23. def OAI.PartitionPilot.Forcing.BoundedFormula.externalFlatStepEntryFormula line 223
  24. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_externalFlatStepEntryFormula line 228
  25. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalFlatStepGraph_mem line 243
  26. theorem OAI.PartitionPilot.Forcing.externalFlatCoordinate_to_step line 294
  27. theorem OAI.PartitionPilot.Forcing.externalFlatTileStep_to_step line 311
  28. theorem OAI.PartitionPilot.Forcing.pair_mem_externalFlatStepGraph_iff line 324
  29. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalVertices line 367
  30. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalOverlaps line 371
  31. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalPlacements line 376
  32. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalFlatSteps line 383
  33. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalFlatEquivalence line 390
  34. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalPointCarrier line 395
  35. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalPointClassifier line 400
  36. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.flat_relations_ground line 415
  37. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.point_quotient_ground line 434
  38. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalFamily_overlapCode_iff line 487
  39. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalFamilyVertexCode_mem_tags line 534
  40. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalOverlaps_same_request line 539
  41. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalOverlaps_entry_iff line 551
  42. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalFamily_vertex_letter line 601
  43. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalFlatVertexWordCode_iff line 657
  44. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalPlacements_entry_iff line 699
  45. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalFlatSteps_iff line 761