OAI/SetTheory/PartitionPrinciple/Geometry/GroundMainBoundTaskOutput.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.compressionActorFamily line 11
2. theorem OAI.PartitionPilot.Forcing.pair_mem_compressionActorFamily line 16
3. def OAI.PartitionPilot.Forcing.BoundedFormula.compressionActorEntryFormula line 30
4. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_compressionActorEntryFormula line 36
5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.compressionActorFamily_mem line 51
6. theorem OAI.PartitionPilot.Forcing.compressionActorFamily_injection line 88
7. theorem OAI.PartitionPilot.Forcing.GroundCompressionOrigin.initial_representatives line 126
8. theorem OAI.PartitionPilot.Forcing.GroundCompressionOrigin.identityTask_representative_agreement line 185
9. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.identityInsertion_source_entry line 222
10. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.identityInsertion_representative_image_agreement line 235
11. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.identityInsertion_generator_fixes line 248
12. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.exists_identityInsertion_actor line 265
13. def OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.insertionActorImages line 310
14. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.insertionActorImages_entry_iff line 314
15. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.insertionActorImages_ground line 339
16. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.insertionActorImages_injection line 351
17. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.insertionActorImages_function line 365
18. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.insertionActorImages_cap_iff line 373
19. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.insertionActorImages_fixes line 406
20. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.insertionActorImages_below_cap line 418
21. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.successorTaskBindings line 453
22. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.boundSuccessorOutput line 461
23. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.realize_boundSuccessorOutput line 467
24. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.insertionFulfillment line 504