OAI/SetTheory/PartitionPrinciple/Geometry/GroundRetainedPreparationSelections.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.PartitionPilot.Forcing.TransitiveGround.retainedPreparationSelectionsline 12 - theorem
OAI.PartitionPilot.Forcing.TransitiveGround.pair_mem_retainedPreparationSelectionsline 19 - def
OAI.PartitionPilot.Forcing.TransitiveGround.selectionBodyline 33 - def
OAI.PartitionPilot.Forcing.TransitiveGround.selectionFormulaline 47 - theorem
OAI.PartitionPilot.Forcing.TransitiveGround.realize_selectionFormulaline 50 - theorem
OAI.PartitionPilot.Forcing.TransitiveGround.retainedPreparationSelections_memline 99 - theorem
OAI.PartitionPilot.Forcing.TransitiveGround.exists_retainedPreparationSelectionline 122