OAI/SetTheory/PartitionPrinciple/Geometry/GroundRefinementVisibleLiftInsertions.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Forcing.TransitiveGround.visibility_forces_upward line 30
2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementVisibleLift_forces_coarse_visibility line 47
3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageOneSingleTests_visible_lift line 80
4. theorem OAI.PartitionPilot.Forcing.stageOneRawTests_insert line 139
5. theorem OAI.PartitionPilot.Forcing.stageOneRawTests_insert_iff line 166
6. theorem OAI.PartitionPilot.Forcing.assignmentCut_insert_current line 199
7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageTwoConditions_insert line 221
8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementLevelRawTests_insert_diagonal line 284
9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementLevelRawTests_dense_diagonal line 321
10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementLevelRawTests_insert_visibleLift line 371
11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementLevelRawTests_dense_visibleLift line 423