OAI/SetTheory/PartitionPrinciple/Transfinite/GroundMainOrdinalConstructionData.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.PartitionPilot.Forcing.TransitiveGround.exists_groundMainOrdinalConstructionline 13 - structure
OAI.PartitionPilot.Forcing.GroundMainOrdinalConstructionDataline 104 - theorem
OAI.PartitionPilot.Forcing.TransitiveGround.exists_groundMainOrdinalDataline 155