OAI/SetTheory/PartitionPrinciple/Forcing/GroundExternalLayerWitnessRanks.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.PartitionPilot.Forcing.GroundExternalBirthData.layerSeparatedCodeline 42 - theorem
OAI.PartitionPilot.Forcing.GroundExternalBirthData.cutoffLayerSeparatedCodeline 69 - theorem
OAI.PartitionPilot.Forcing.GroundExternalBirthData.layerWitness_specline 99 - theorem
OAI.PartitionPilot.Forcing.GroundExternalBirthData.cutoffLayerWitness_specline 109 - theorem
OAI.PartitionPilot.Forcing.GroundExternalBirthData.layerWitness_rank_ltline 144 - theorem
OAI.PartitionPilot.Forcing.GroundExternalBirthData.ranked_layerWitness_specline 170 - theorem
OAI.PartitionPilot.Forcing.GroundExternalBirthData.ranked_cutoffLayerWitness_specline 180