OAI/SetTheory/PartitionPrinciple/Definability/GroundBelowMainGraphs.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Forcing.GroundMainStage.height_below line 20
2. theorem OAI.PartitionPilot.Forcing.GroundMainStage.inverse_below line 25
3. theorem OAI.PartitionPilot.Forcing.GroundMainStage.order_below line 30
4. theorem OAI.PartitionPilot.Forcing.GroundMainStage.meetGraph_below line 35
5. theorem OAI.PartitionPilot.Forcing.GroundMainStage.multiplication_below line 42
6. theorem OAI.PartitionPilot.Forcing.GroundMainStage.action_below line 49
7. theorem OAI.PartitionPilot.Forcing.GroundMainStage.graphs_below line 57
8. theorem OAI.PartitionPilot.Forcing.GroundChronologicalMainStage.birth_below line 73
9. theorem OAI.PartitionPilot.Forcing.GroundMainTransition.graphs_below line 82