OAI/SetTheory/PartitionPrinciple/Transfinite/GroundBinaryRowStageOneRefinement.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.PartitionPilot.Forcing.RefinementStageSystem line 13
2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementStageSystem line 33
3. structure OAI.PartitionPilot.Forcing.StageTwoIndexData line 71
4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageTwoForcing_entry line 117
5. structure OAI.PartitionPilot.Forcing.StageTwoCarrierData line 148
6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageTwoCarrierData line 201
7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageOneRefinementStageSystem line 261
8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.binaryRowStageOneRefinement line 312