OAI/SetTheory/PartitionPrinciple/Definability/GroundBoundedExternalBirths.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalBoundedCarrier line 16
2. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalBoundedOrder line 19
3. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalBoundedMeet line 22
4. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalBoundedAction line 25
5. structure OAI.PartitionPilot.Forcing.GroundExternalBoundedGeometryData line 31
6. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalBoundedGeometryData line 80
7. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalBoundedCopy_bottom line 95
8. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalBoundedOriginal_agreement line 104
9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_groundInitialExternalBoundedGeometry line 125
10. theorem OAI.PartitionPilot.Forcing.GroundProfiledCompression.external_bounded_generator_profile line 201
11. def OAI.PartitionPilot.Forcing.GroundExternalHeightData.boundedHeight line 263
12. theorem OAI.PartitionPilot.Forcing.GroundExternalHeightData.attained_columns_below line 266
13. structure OAI.PartitionPilot.Forcing.GroundBoundedExternalHeightData line 277
14. theorem OAI.PartitionPilot.Forcing.GroundExternalHeightData.boundedData line 306
15. def OAI.PartitionPilot.Forcing.GroundExternalBirthData.boundedBirth line 349
16. structure OAI.PartitionPilot.Forcing.GroundBoundedExternalBirthData line 354
17. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.boundedData line 384
18. def OAI.PartitionPilot.Forcing.GroundExternalBirthData.bounded_incoming_layer line 410