OAI/SetTheory/PartitionPrinciple/Definability/IndexedOperationLiftCodes.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.indexedRelationLift line 12
2. theorem OAI.PartitionPilot.Forcing.indexedRelationLift_subset line 19
3. theorem OAI.PartitionPilot.Forcing.pair_mem_indexedRelationLift line 23
4. def OAI.PartitionPilot.Forcing.indexedBinaryLift line 38
5. theorem OAI.PartitionPilot.Forcing.indexedBinaryLift_subset line 45
6. theorem OAI.PartitionPilot.Forcing.triple_mem_indexedBinaryLift line 49
7. theorem OAI.PartitionPilot.Forcing.indexedRelationLift_rank_lt line 70
8. theorem OAI.PartitionPilot.Forcing.indexedBinaryLift_rank_lt line 76