OAI/SetTheory/PartitionPrinciple/Definability/GroundExternalRequestSetRecognition.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.externalRequestCarrier line 10
  2. def OAI.PartitionPilot.Forcing.externalChildLetters line 14
  3. theorem OAI.PartitionPilot.Forcing.pair_mem_externalRequestCarrier line 18
  4. theorem OAI.PartitionPilot.Forcing.compression_mem_externalRequestCarrier line 25
  5. theorem OAI.PartitionPilot.Forcing.separation_mem_externalRequestCarrier line 31
  6. theorem OAI.PartitionPilot.Forcing.rectangle_mem_externalRequestCarrier line 37
  7. theorem OAI.PartitionPilot.Forcing.pair_mem_externalChildLetters line 43
  8. theorem OAI.PartitionPilot.Forcing.compression_child_iff line 49
  9. theorem OAI.PartitionPilot.Forcing.separation_child_iff line 56
  10. theorem OAI.PartitionPilot.Forcing.rectangle_child_iff line 63
  11. def OAI.PartitionPilot.Forcing.externalRequestTags line 70
  12. def OAI.PartitionPilot.Forcing.externalRequestPayloadBound line 73
  13. theorem OAI.PartitionPilot.Forcing.externalRequestCarrier_subset line 76
  14. def OAI.PartitionPilot.Forcing.externalRequestKinds line 99
  15. def OAI.PartitionPilot.Forcing.externalRequestPayloads line 103
  16. theorem OAI.PartitionPilot.Forcing.externalRequestKinds_function line 107
  17. theorem OAI.PartitionPilot.Forcing.externalRequestPayloads_function line 113
  18. theorem OAI.PartitionPilot.Forcing.externalRequest_fields_entry line 119
  19. def OAI.PartitionPilot.Forcing.ExternalRequestOverlapForward line 130
  20. def OAI.PartitionPilot.Forcing.ExternalRequestOverlapCode line 140
  21. theorem OAI.PartitionPilot.Forcing.ExternalRequestOverlapCode.symm line 146
  22. def OAI.PartitionPilot.Forcing.externalTileVertices line 155
  23. theorem OAI.PartitionPilot.Forcing.triple_mem_externalTileVertices line 159
  24. def OAI.PartitionPilot.Forcing.BoundedFormula.compressionOverlapFormula line 170
  25. def OAI.PartitionPilot.Forcing.BoundedFormula.separationOverlapFormula line 175
  26. def OAI.PartitionPilot.Forcing.BoundedFormula.requestRectangleOverlapFieldsFormula line 180
  27. def OAI.PartitionPilot.Forcing.BoundedFormula.requestRectangleOverlapFormula line 188
  28. def OAI.PartitionPilot.Forcing.BoundedFormula.externalRequestOverlapForwardFormula line 199
  29. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_externalRequestOverlapForwardFormula line 205
  30. def OAI.PartitionPilot.Forcing.BoundedFormula.externalRequestOverlapFormula line 216
  31. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_externalRequestOverlapFormula line 222
  32. abbrev OAI.PartitionPilot.Forcing.ExternalRequestIndex line 238
  33. def OAI.PartitionPilot.Forcing.externalRequestIndexCode line 241
  34. theorem OAI.PartitionPilot.Forcing.externalRequestIndexCode_injective line 247
  35. def OAI.PartitionPilot.Forcing.externalRequestPresentation line 255
  36. def OAI.PartitionPilot.Forcing.ExternalRequestChild line 279
  37. def OAI.PartitionPilot.Forcing.externalRequestChildCode line 284
  38. theorem OAI.PartitionPilot.Forcing.externalRequestChildCode_injective line 290
  39. theorem OAI.PartitionPilot.Forcing.externalRequestChildCode_range line 300
  40. def OAI.PartitionPilot.Forcing.externalRequestLetterCode line 322
  41. theorem OAI.PartitionPilot.Forcing.externalRequestLetterCode_injective line 326
  42. def OAI.PartitionPilot.Forcing.externalRequestLetterPresentation line 336
  43. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalRectangleBound_mem line 371
  44. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalRectangles_mem line 377
  45. theorem OAI.PartitionPilot.Forcing.TransitiveGround.tag_mem line 395
  46. theorem OAI.PartitionPilot.Forcing.TransitiveGround.singleton_mem line 401
  47. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalRequestCarrier_mem line 404
  48. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalChildLetters_mem line 414
  49. theorem OAI.PartitionPilot.Forcing.TransitiveGround.fieldBounds_mem line 427
  50. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalRequestKinds_mem line 435
  51. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalRequestPayloads_mem line 443
  52. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundExternalRequestData line 451
  53. def OAI.PartitionPilot.Forcing.BoundedFormula.externalRequestSetEntryFormula line 476
  54. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_externalRequestSetEntryFormula line 481
  55. def OAI.PartitionPilot.Forcing.BoundedFormula.externalChildSetEntryFormula line 489
  56. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_externalChildSetEntryFormula line 493
  57. def OAI.PartitionPilot.Forcing.SetFormula.externalRectanglesSetFormula line 507
  58. def OAI.PartitionPilot.Forcing.SetFormula.externalRequestSetFormula line 511
  59. def OAI.PartitionPilot.Forcing.SetFormula.externalChildSetFormula line 516
  60. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_externalRectanglesSetFormula line 530
  61. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_externalRequestSetFormula line 547
  62. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_externalChildSetFormula line 560