OAI/Computability/DegreeRigidity/SetModels/SkolemOperations.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TuringRigidity.BoundedSetTheory.FiniteTerm.labelGraph line 12
2. theorem OAI.TuringRigidity.BoundedSetTheory.FiniteTerm.labelGraph_mem line 16
3. theorem OAI.TuringRigidity.BoundedSetTheory.FiniteTerm.labelGraph_shape line 30
4. theorem OAI.TuringRigidity.BoundedSetTheory.FiniteTerm.labelGraph_contains line 34
5. theorem OAI.TuringRigidity.BoundedSetTheory.FiniteTerm.labelGraph_functional line 41
6. theorem OAI.TuringRigidity.BoundedSetTheory.FiniteTerm.Functional.union line 52
7. theorem OAI.TuringRigidity.BoundedSetTheory.FiniteTerm.skolem_functional line 61
8. theorem OAI.TuringRigidity.BoundedSetTheory.FiniteTerm.internal_skolem_operations line 70