OAI/SetTheory/PartitionPrinciple/Geometry/GroundSerializedCandidateLevels.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.PartitionPilot.Forcing.GroundMainCandidateLevel line 10
2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_groundMainCandidateLevel line 22
3. theorem OAI.PartitionPilot.Forcing.GroundMainCandidateLevel.stage_mem line 46
4. theorem OAI.PartitionPilot.Forcing.GroundMainCandidateLevel.birth_mem line 53
5. theorem OAI.PartitionPilot.Forcing.GroundMainCandidateLevel.transition_mem line 60
6. theorem OAI.PartitionPilot.Forcing.GroundMainCandidateLevel.relationSpace_ground line 69
7. def OAI.PartitionPilot.Forcing.GroundMainCandidateLevel.validStages line 84
8. theorem OAI.PartitionPilot.Forcing.GroundMainCandidateLevel.validStages_ground line 87
9. theorem OAI.PartitionPilot.Forcing.GroundMainCandidateLevel.invariant_mem_validStages line 96
10. theorem OAI.PartitionPilot.Forcing.GroundMainCandidateLevel.validStageFamily_rank_lt line 107
11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_groundMainSeedCandidates line 128
12. def OAI.PartitionPilot.Forcing.GroundMainCandidateLevel.validChronologies line 169
13. theorem OAI.PartitionPilot.Forcing.GroundMainCandidateLevel.validChronologies_ground line 172
14. theorem OAI.PartitionPilot.Forcing.GroundMainCandidateLevel.ranked_mem_validChronologies line 182
15. theorem OAI.PartitionPilot.Forcing.GroundMainCandidateLevel.validChronologyFamily_rank_lt line 190
16. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_groundInitialChronologyCandidates line 211