OAI/SetTheory/PartitionPrinciple/Geometry/RectangleFulfillmentAtBound.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.externalRectangleCode line 9
  2. def OAI.PartitionPilot.Forcing.externalRectangleBound line 12
  3. def OAI.PartitionPilot.Forcing.ExternalRectangleCode line 15
  4. def OAI.PartitionPilot.Forcing.externalRectangles line 23
  5. theorem OAI.PartitionPilot.Forcing.externalRectangleCode_inj line 28
  6. theorem OAI.PartitionPilot.Forcing.externalRectangleCode_mem_bound line 33
  7. theorem OAI.PartitionPilot.Forcing.mem_externalRectangles line 38
  8. theorem OAI.PartitionPilot.Forcing.externalRectangleCode_mem line 50
  9. def OAI.PartitionPilot.Forcing.BoundedFormula.actionAgreementBelowFormula line 64
  10. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_actionAgreementBelowFormula line 71
  11. def OAI.PartitionPilot.Forcing.BoundedFormula.rectangleSeparatedFormula line 79
  12. def OAI.PartitionPilot.Forcing.BoundedFormula.externalRectangleFormula line 86
  13. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_externalRectangleFormula line 93
  14. def OAI.PartitionPilot.Forcing.BoundedFormula.externalRectangleTupleFormula line 103
  15. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_externalRectangleTupleFormula line 107
  16. def OAI.PartitionPilot.Forcing.BoundedFormula.externalRectanglesEntryFormula line 114
  17. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_externalRectanglesEntryFormula line 122
  18. def OAI.PartitionPilot.Forcing.CompressionActorCode line 138
  19. def OAI.PartitionPilot.Forcing.CompressionActorFulfillmentCode line 147
  20. def OAI.PartitionPilot.Forcing.BoundedFormula.compressionActorFormula line 153
  21. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_compressionActorFormula line 171
  22. def OAI.PartitionPilot.Forcing.BoundedFormula.compressionActorFulfillmentFormula line 181
  23. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_compressionActorFulfillmentFormula line 188
  24. theorem OAI.PartitionPilot.Forcing.BoundedFormula.realize_compressionActorFulfillmentFormula line 196
  25. def OAI.PartitionPilot.Forcing.ExternalRectangleCode.toActionRectangle line 218
  26. theorem OAI.PartitionPilot.Forcing.ExternalRectangleCode.toActionRectangle_fields line 262
  27. theorem OAI.PartitionPilot.Forcing.externalRectangleCode_of_actionRectangle line 270
  28. theorem OAI.PartitionPilot.Forcing.actionRectangle_mem_externalRectangles line 296
  29. def OAI.PartitionPilot.Forcing.RectangleIdealCode line 310
  30. def OAI.PartitionPilot.Forcing.RectangleRootMeetCode line 316
  31. def OAI.PartitionPilot.Forcing.RectangleCrossMeetCode line 322
  32. def OAI.PartitionPilot.Forcing.RectangleActorPairCode line 329
  33. def OAI.PartitionPilot.Forcing.RectangleFulfillmentCode line 335
  34. def OAI.PartitionPilot.Forcing.BoundedFormula.rectangleIdealFormula line 342
  35. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_rectangleIdealFormula line 345
  36. def OAI.PartitionPilot.Forcing.BoundedFormula.rectangleRootMeetFormula line 352
  37. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_rectangleRootMeetFormula line 355
  38. def OAI.PartitionPilot.Forcing.BoundedFormula.rectangleCrossMeetFormula line 362
  39. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_rectangleCrossMeetFormula line 365
  40. def OAI.PartitionPilot.Forcing.BoundedFormula.rectangleActorPairFormula line 372
  41. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_rectangleActorPairFormula line 375
  42. def OAI.PartitionPilot.Forcing.BoundedFormula.rectangleFulfillmentFormula line 382
  43. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_rectangleFulfillmentFormula line 385
  44. theorem OAI.PartitionPilot.Forcing.BoundedFormula.realize_rectangleFulfillmentFormula line 392
  45. theorem OAI.PartitionPilot.Forcing.TransitiveGround.choose_compressionActorFamily line 410
  46. structure OAI.PartitionPilot.Forcing.RectangleAtBoundCode line 453
  47. theorem OAI.PartitionPilot.Forcing.MeetOrderCode.meet_entry_of_lower line 464
  48. theorem OAI.PartitionPilot.Forcing.GroundMainTransition.rectangle_at_bound line 483