OAI/SetTheory/PartitionPrinciple/Transfinite/GroundMainStageInvariant.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundInitialExternalLetters_below line 25
2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundInitialExternalGroup_below line 37
3. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.compression_union_below line 69
4. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.target_below line 76
5. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.transition_graphs_below line 106
6. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.target_graphs_below line 112
7. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.standard_bounds line 141
8. structure OAI.PartitionPilot.Forcing.GroundChronologicalMainStage.Invariant line 187
9. theorem OAI.PartitionPilot.Forcing.GroundChronologicalMainStage.Invariant.code_rank_lt line 208
10. theorem OAI.PartitionPilot.Forcing.GroundChronologicalMainStage.Invariant.birth_rank_lt line 212
11. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSuccessorData.target_invariant line 226