OAI/SetTheory/PartitionPrinciple/Forcing/GroundIdealProjections.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.PartitionPilot.Forcing.idealProjectionGraphline 11 - theorem
OAI.PartitionPilot.Forcing.TransitiveGround.idealProjectionGraph_memline 16 - theorem
OAI.PartitionPilot.Forcing.idealProjectionGraph_pair_iffline 37 - theorem
OAI.PartitionPilot.Forcing.idealProjectionGraph_eqline 66 - theorem
OAI.PartitionPilot.Forcing.TransitiveGround.idealProjection_memline 83