OAI/SetTheory/PartitionPrinciple/Definability/TupleRelationProducts.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.tupleRelationBound line 13
2. def OAI.PartitionPilot.Forcing.tupleRelationProduct line 17
3. theorem OAI.PartitionPilot.Forcing.mem_tupleRelationBound line 23
4. theorem OAI.PartitionPilot.Forcing.pair_mem_tupleRelationProduct line 33
5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.tupleRelationBound_mem line 60
6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.tupleRelationProduct_mem line 68