OAI/SetTheory/PartitionPrinciple/Geometry/MainRectangleMeets.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Transition.Separates line 16
  2. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Transition.separates_transport line 21
  3. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.separationActor line 30
  4. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.separation_internal line 33
  5. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.separation_fixes_ideal line 49
  6. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.separation_meet line 56
  7. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.next_separates line 79
  8. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.rectangleOldActor line 93
  9. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.rectangleActor line 95
  10. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.rectangleInput line 98
  11. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.rectangle_internal_C line 102
  12. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.rectangle_internal_B line 127
  13. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.rectangle_agrees_C line 152
  14. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.rectangle_agrees_B line 161
  15. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.rectangle_meet_internal line 178
  16. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.rectangle_meet_root line 207
  17. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.rectangle_meet_pair line 226
  18. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Transition.Rectangles line 259
  19. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Transition.rectangles_transport line 271
  20. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.next_rectangles line 277
  21. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.stage_successor_separates line 290
  22. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.final_separation_at line 297
  23. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.final_separation line 321