OAI/SetTheory/PartitionPrinciple/Transfinite/GroundMainPrefixPreservedSeeds.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.GroundMainPrefix.ofFinite line 22
2. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.finite_stageGraph_rank_lt line 54
3. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.transition_code_rank_lt line 59
4. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.finite_transitionGraph_rank_lt line 68
5. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.finite_code_rank_lt line 74
6. def OAI.PartitionPilot.Forcing.GroundMainPrefix.twoStage line 96
7. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.twoStage_indices line 116
8. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.twoStage_linked_zero line 120
9. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.twoStage_linked_one line 123
10. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.twoStage_stage_zero line 126
11. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.twoStage_stage_one line 129
12. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.twoStage_transition_zero_one line 132
13. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.twoStage_stageGraph_zero line 136
14. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.twoStage_stageGraph_one line 141
15. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.twoStage_transitionGraph_zero_one line 146
16. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.twoStage_code_rank_lt line 152
17. def OAI.PartitionPilot.Forcing.GroundChronologicalMainTransition.PreservesOldProfiles line 172
18. theorem OAI.PartitionPilot.Forcing.GroundChronologicalMainTransition.identity_preservesOldProfiles line 177
19. theorem OAI.PartitionPilot.Forcing.GroundChronologicalMainTransition.comp_preservesOldProfiles line 186
20. theorem OAI.PartitionPilot.Forcing.GroundChronologicalMainTransition.retargetEq_preservesOldProfiles_iff line 197
21. theorem OAI.PartitionPilot.Forcing.TaskBearingMainSuccessorCode.preservesOldProfiles line 212
22. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_groundInitialTwoStageMainPrefix line 228
23. def OAI.PartitionPilot.Forcing.GroundMainPrefix.PreservesOldProfiles line 309
24. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.restrict_preservesOldProfiles line 312
25. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.zero_key_of_two_indices line 332
26. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.exists_initialRestriction line 343
27. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.appendCone_preservesOldProfiles line 389
28. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.appendLast_preservesOldProfiles line 409
29. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.preservesOldProfiles_of_zero_one line 443
30. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.twoStage_preservesOldProfiles line 469