OAI/SetTheory/PartitionPrinciple/Geometry/GroundInitialCompressionCompletion.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.initial_map_marks line 21
2. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.union_initial_old_shadow line 52
3. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.union_initial_cap_separation line 85
4. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.union_map_target line 142
5. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.union_caps_common_target_meet line 164
6. theorem OAI.PartitionPilot.Forcing.GroundCompressionOrigin.union_caps_common_target_meet line 211
7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_groundInitialCompressionCompletion line 250