OAI/SetTheory/PartitionPrinciple/Transfinite/GroundLinkedMainStageLevels.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.SetFormula.linkedMainStageFormula line 12
2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_linkedMainStageFormula_raw line 26
3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_linkedMainStageFormula line 47
4. def OAI.PartitionPilot.Forcing.TransitiveGround.linkedMainStageCandidates line 63
5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.mem_linkedMainStageCandidates line 67
6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.linkedMainStageCandidates_mem line 71
7. def OAI.PartitionPilot.Forcing.GroundMainCandidateLevel.validLinkedStages line 104
8. theorem OAI.PartitionPilot.Forcing.GroundMainCandidateLevel.validLinkedStages_ground line 107
9. theorem OAI.PartitionPilot.Forcing.GroundMainCandidateLevel.mem_validLinkedStages line 118
10. theorem OAI.PartitionPilot.Forcing.GroundMainCandidateLevel.linked_mem_validLinkedStages line 123
11. theorem OAI.PartitionPilot.Forcing.GroundMainCandidateLevel.validLinkedStageFamily_rank_lt line 134