OAI/SetTheory/PartitionPrinciple/Transfinite/GroundOmegaOneTaskBearingSuccessorFunction.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.exists_rankedTargetSerialization line 26
2. def OAI.PartitionPilot.Forcing.SetFormula.taskBearingSuccessorPairFormula line 80
3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_taskBearingSuccessorPairFormula line 92
4. def OAI.PartitionPilot.Forcing.TransitiveGround.taskBearingSuccessorParams line 122
5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.taskBearingSuccessorParams_ground line 126
6. def OAI.PartitionPilot.Forcing.TransitiveGround.taskBearingSuccessorRelation line 135
7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.taskBearingSuccessorRelation_ground line 139
8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.taskBearingSuccessorRelation_entry line 152
9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.choose_taskBearingSuccessors line 181
10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_groundInitialMainSeedSuccessorRanked line 221
11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_rankedTaskBearingSuccessor line 296
12. theorem OAI.PartitionPilot.Forcing.TransitiveGround.omegaOne_taskBearingSuccessor_total line 330
13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_groundOmegaOneTaskBearingSuccessorFunction line 360