OAI/SetTheory/PartitionPrinciple/Geometry/GroundPreparedPositionCollisions.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Forcing.TransitiveGround.niceRefinementIndex_copies_agree line 21
2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.niceRefinementIndex_copies_agree_of_shared_anchor line 48
3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementLevelFormulaData_fields line 89
4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementLevelFormulaData_map line 106
5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementLevelFormulaData_visibility line 118
6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementLevelRawCollision_iff line 142
7. theorem OAI.PartitionPilot.Forcing.GroundMainFinalGeometry.copied_refinement_index_shared_anchor line 201
8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.prepared_joint_refinementCollision_tests line 273
9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.prepared_refinementCollision_tests line 407
10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.prepared_joint_refinementCollision_of_position_supports line 542