OAI/SetTheory/PartitionPrinciple/Geometry/InitialCompressionUnionProfiles.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.original_positive_iff line 12
2. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.initial_cap_profile line 25
3. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.fresh_shadow_separation line 62
4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundEligibleTask_old_below_cap_iff line 101
5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundEligibleTask_cap_separation line 120
6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundInitialMap_cap_base_values line 156
7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundInitialMap_old_below_cap_iff line 175
8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundInitialMap_cap_separation line 196
9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundEligibleTask_initial_profile line 238
10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundInitialMap_profile line 300
11. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.union_profile line 345
12. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.union_separator_not_below_cap line 361
13. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.union_input_capProfile line 382
14. theorem OAI.PartitionPilot.Forcing.GroundCompressionOrigin.union_input_capProfile line 424
15. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.union_initial_profile line 457
16. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.initial_union_profiles line 504