OAI/SetTheory/PartitionPrinciple/Geometry/GroundInitialSeedSerializationRanks.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Forcing.fractionCarrier_rank_lt line 12
2. theorem OAI.PartitionPilot.Forcing.rationalCarrier_rank_lt line 20
3. theorem OAI.PartitionPilot.Forcing.rationalLtGraph_rank_lt line 25
4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.rational_seed_pair line 35
5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_groundRationalSeed line 43
6. structure OAI.PartitionPilot.Forcing.GroundInitialMainSeedData line 87
7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.initialMainChronological_invariant line 124
8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_groundInitialMainSeed line 138
9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_groundInitialMainSeedSerialized line 193
10. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSeedData.initialSerializedChronology_code_rank_lt line 240
11. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSeedData.exists_rankedInitialSerialization line 251