OAI/SetTheory/PartitionPrinciple/Forcing/GroundNiceNameGraphs.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.PartitionPilot.Forcing.TransitiveGround.niceNameCandidateGraphline 13 - theorem
OAI.PartitionPilot.Forcing.TransitiveGround.mem_niceNameCandidateGraphline 16 - theorem
OAI.PartitionPilot.Forcing.TransitiveGround.pair_mem_niceNameCandidateGraphline 22 - theorem
OAI.PartitionPilot.Forcing.TransitiveGround.niceNameCandidateGraph_functionline 27 - theorem
OAI.PartitionPilot.Forcing.TransitiveGround.niceNameCandidates_eq_selectionline 37 - theorem
OAI.PartitionPilot.Forcing.TransitiveGround.niceNameCandidateGraph_memline 70