OAI/SetTheory/PartitionPrinciple/Transfinite/GroundInitialMainSeedSuccessorSerialization.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.GroundSerializedChronology.fixedTopValues line 14
2. theorem OAI.PartitionPilot.Forcing.GroundSerializedChronology.fixedTopValues_ground line 27
3. def OAI.PartitionPilot.Forcing.GroundSerializedChronology.fixedTopFields line 37
4. theorem OAI.PartitionPilot.Forcing.GroundSerializedChronology.fixedTopFields_value_at line 41
5. theorem OAI.PartitionPilot.Forcing.GroundSerializedChronology.fixedTopFields_value_old line 46
6. theorem OAI.PartitionPilot.Forcing.GroundSerializedChronology.fixedTopFields_value line 51
7. theorem OAI.PartitionPilot.Forcing.GroundSerializedChronology.fixedTopFields_old_entries line 56
8. theorem OAI.PartitionPilot.Forcing.GroundSerializedChronology.fixedTopFields_core line 61
9. theorem OAI.PartitionPilot.Forcing.GroundSerializedChronology.fixedTopFields_rawWitnesses line 116
10. theorem OAI.PartitionPilot.Forcing.GroundSerializedChronology.exists_fixedTopSerialization line 177
11. theorem OAI.PartitionPilot.Forcing.GroundSerializedChronology.exists_fixedTopSerialization_values line 191
12. theorem OAI.PartitionPilot.Forcing.GroundChronologicalHistory.fieldValue_eq_of_heq line 215
13. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.exists_compressionSerialization line 242
14. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.exists_externalSerialization line 257
15. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.exists_boundedSerialization line 309
16. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.exists_targetSerialization line 360
17. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.compression_history_carrier_rank_lt line 418
18. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.external_history_carrier_rank_lt line 432
19. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.target_history_carrier_rank_lt line 448
20. theorem OAI.PartitionPilot.Forcing.GroundSerializedChronology.agreeing_history_carrier_rank_lt line 476
21. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.compressionFieldGraphs_rank_lt line 507
22. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.externalFieldGraphs_rank_lt line 522
23. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.targetFieldGraphs_rank_lt line 541
24. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_groundInitialMainSeedSuccessor line 569
25. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_groundInitialMainSeedSuccessorSerialized line 602