OAI/SetTheory/PartitionPrinciple/Geometry/GroundRequestedRectangleHeights.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.rectangleLabelCarrier line 11
  2. def OAI.PartitionPilot.Forcing.rectangleOverlapRel line 14
  3. def OAI.PartitionPilot.Forcing.rectangleOverlapGraph line 23
  4. theorem OAI.PartitionPilot.Forcing.mem_rectangleOverlapGraph line 28
  5. theorem OAI.PartitionPilot.Forcing.pair_mem_rectangleOverlapGraph line 39
  6. theorem OAI.PartitionPilot.Forcing.rectangleOverlapGraph_subset line 52
  7. def OAI.PartitionPilot.Forcing.BoundedFormula.localRectangleOverlapFormula line 59
  8. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_localRectangleOverlapFormula line 72
  9. def OAI.PartitionPilot.Forcing.BoundedFormula.rectangleOverlapEntryFormula line 80
  10. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_rectangleOverlapEntryFormula line 87
  11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.rectangleOverlapGraph_mem line 116
  12. def OAI.PartitionPilot.Forcing.rectangleVertexCode line 154
  13. theorem OAI.PartitionPilot.Forcing.rectangleVertexCode_injective line 159
  14. theorem OAI.PartitionPilot.Forcing.rectangleVertexCode_mem line 163
  15. theorem OAI.PartitionPilot.Forcing.mem_three_iff_rectangleVertexCode line 166
  16. def OAI.PartitionPilot.Forcing.rectangleLabelPresentation line 179
  17. theorem OAI.PartitionPilot.Forcing.rectangleOverlapRel_iff line 204
  18. theorem OAI.PartitionPilot.Forcing.rectangleOverlapGraph_iff line 233
  19. theorem OAI.PartitionPilot.Forcing.rectangleOverlap_equivalence line 244
  20. def OAI.PartitionPilot.Forcing.rectangleTilePresentation line 266
  21. def OAI.PartitionPilot.Forcing.rectangleQuotientOrder line 277
  22. theorem OAI.PartitionPilot.Forcing.mem_rectangleQuotientOrder line 284
  23. theorem OAI.PartitionPilot.Forcing.pair_mem_rectangleQuotientOrder line 297
  24. theorem OAI.PartitionPilot.Forcing.rectangleQuotientOrder_subset line 310
  25. abbrev OAI.PartitionPilot.Forcing.rectangleTileOrder line 320
  26. theorem OAI.PartitionPilot.Forcing.rectangleTileOrder_iff line 327
  27. theorem OAI.PartitionPilot.Forcing.rectangleTile_partialOrder line 351
  28. theorem OAI.PartitionPilot.Forcing.rectangleTile_meet_glb line 370
  29. theorem OAI.PartitionPilot.Forcing.rectangleTile_meetOrder line 384
  30. theorem OAI.PartitionPilot.Forcing.rectangleTile_meet_entry line 397
  31. def OAI.PartitionPilot.Forcing.BoundedFormula.rectangleQuotientOrderFormula line 415
  32. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_rectangleQuotientOrderFormula line 423
  33. theorem OAI.PartitionPilot.Forcing.TransitiveGround.rectangleQuotientOrder_mem line 437
  34. theorem OAI.PartitionPilot.Forcing.TransitiveGround.rectangleTile_ground line 465
  35. def OAI.PartitionPilot.Forcing.rectangleTileVertexGraph line 499
  36. theorem OAI.PartitionPilot.Forcing.rectangleTileVertexGraph_iff line 507
  37. theorem OAI.PartitionPilot.Forcing.rectangleTileVertexGraph_eq line 516
  38. theorem OAI.PartitionPilot.Forcing.rectangleTileVertex_injection line 526
  39. theorem OAI.PartitionPilot.Forcing.rectangleTileVertex_order_iff line 532
  40. theorem OAI.PartitionPilot.Forcing.rectangleTileVertex_embedding line 544
  41. theorem OAI.PartitionPilot.Forcing.rectangleTileVertex_cover line 572
  42. theorem OAI.PartitionPilot.Forcing.rectangleTileVertex_overlap line 580
  43. theorem OAI.PartitionPilot.Forcing.rectangleTileVertex_ideal line 587
  44. theorem OAI.PartitionPilot.Forcing.TransitiveGround.rectangleTileVertexGraph_mem line 596
  45. theorem OAI.PartitionPilot.Forcing.PosetActionCode.section_small_iff line 624
  46. theorem OAI.PartitionPilot.Forcing.ExternalRectangleCode.exists_ground_tile line 632
  47. theorem OAI.PartitionPilot.Forcing.ExternalRectangleCode.exists_ground_height line 705