OAI/SetTheory/PartitionPrinciple/Forcing/GroundFlatSuccessorNameGraphs.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.TransitiveGround.flatSuccessorNameLift line 21
2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.flatSuccessorNameLift_val line 27
3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.flatSuccessorNameLift_mem line 32
4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.flatSuccessorNameLift_eval line 37
5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.flatSuccessorSmallInclusion_graph line 68
6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.flatSuccessorSmallInclusion_graph_mem line 85
7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.flatSuccessorNameLiftGraph_eq line 92
8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.flatSuccessorNameLiftGraph_mem line 109
9. def OAI.PartitionPilot.Forcing.TransitiveGround.flatSuccessorGroundNameLift line 117
10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.flatSuccessorGroundNameLift_val line 120