OAI/SetTheory/PartitionPrinciple/Definability/GroundNiceVisibilityGraphs.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.PartitionPilot.Forcing.TransitiveGround.niceVisibilityGraphline 14 - theorem
OAI.PartitionPilot.Forcing.TransitiveGround.mem_niceVisibilityGraphline 17 - theorem
OAI.PartitionPilot.Forcing.TransitiveGround.pair_mem_niceVisibilityGraphline 23 - theorem
OAI.PartitionPilot.Forcing.TransitiveGround.niceVisibilityGraph_functionline 28 - theorem
OAI.PartitionPilot.Forcing.TransitiveGround.niceVisibilityGraph_memline 38