OAI/SetTheory/PartitionPrinciple/Transfinite/GroundExternalBirthLayers.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Forcing.pushedBirthGraph_oldMeet line 11
2. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalSeedBirth line 46
3. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalSeedBirth_spec line 68
4. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalSeedBirth_entry line 80
5. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalBirthGraph line 98
6. structure OAI.PartitionPilot.Forcing.GroundExternalBirthData line 105
7. def OAI.PartitionPilot.Forcing.GroundExternalBirthData.birth line 129
8. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.old_before line 133
9. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.stamp_fiber line 138
10. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.no_limit_birth line 148
11. def OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalBirthCopyVertex line 181
12. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalBirthCopyVertex_eq line 185
13. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalBirthCopy_witness line 195
14. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.exists_externalBirths_of_seed line 245
15. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.exists_externalBirths line 289
16. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalBirthCopy_level_slot line 330
17. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalBirthCopy_level_bound line 357
18. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalBirthCopy_image_level_bound line 382
19. def OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalBirth_fresh_layer line 426