OAI/SetTheory/PartitionPrinciple/Geometry/GroundGrowthLayerRecognition.lean
9 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.PartitionPilot.Forcing.SetFormula.countableGrowthWitnessFormulaline 15 - def
OAI.PartitionPilot.Forcing.SetFormula.copyGrowthWitnessFormulaline 21 - def
OAI.PartitionPilot.Forcing.SetFormula.separatedGrowthWitnessFormulaline 29 - def
OAI.PartitionPilot.Forcing.SetFormula.growthLayerWitnessFormulaline 37 - theorem
OAI.PartitionPilot.Forcing.TransitiveGround.realize_boundedExBlockline 46 - theorem
OAI.PartitionPilot.Forcing.TransitiveGround.realize_countableGrowthWitnessFormulaline 60 - theorem
OAI.PartitionPilot.Forcing.TransitiveGround.realize_copyGrowthWitnessFormulaline 87 - theorem
OAI.PartitionPilot.Forcing.TransitiveGround.realize_separatedGrowthWitnessFormulaline 132 - theorem
OAI.PartitionPilot.Forcing.TransitiveGround.realize_growthLayerWitnessFormulaline 187