OAI/SetTheory/PartitionPrinciple/Transfinite/GroundExternalSerializedChronology.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.serialized_old_raw_witness line 35
2. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.serialized_base_entries line 67
3. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.serialized_base_raw_witness line 78
4. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.serialized_finite_raw_witness line 88
5. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.serialized_limit_raw_witness line 118
6. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.serialized_all_raw_witnesses line 151
7. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.ranked_prior_source_entries line 197
8. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.serialized_old_ranked_raw_witness line 210
9. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.serialized_terminal_prior_ranked_witness line 241
10. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.serialized_all_ranked_raw_witnesses line 254
11. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.exists_externalSerializedChronology line 384