OAI/SetTheory/PartitionPrinciple/Geometry/GroundAssignmentRepresentativeClosure.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Forcing.assignmentOnIndices_indices_on line 11
2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.assignmentQueryRelation_mem line 42
3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realizedAssignmentQueries_mem line 63
4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_assignmentQuerySelector line 69
5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_stageOneAssignmentQuerySelector line 81
6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_groundOmegaOneClosure line 98
7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.assignmentQueryClosure_representatives line 167
8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_assignmentRepresentativeClosure line 222