OAI/Computability/DegreeRigidity/SetModels/ElementaryDegreeHull.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TuringRigidity.ElementaryModel.witness_in_hull line 10
2. theorem OAI.TuringRigidity.ElementaryModel.degree_representative_in_hull line 20
3. theorem OAI.TuringRigidity.ElementaryModel.degreeSet_fixed line 29
4. theorem OAI.TuringRigidity.ElementaryModel.pair_components_mem_hull line 43
5. def OAI.TuringRigidity.ElementaryModel.globalGraph line 61
6. theorem OAI.TuringRigidity.ElementaryModel.mem_globalGraph line 64
7. theorem OAI.TuringRigidity.ElementaryModel.globalGraph_pair line 69
8. theorem OAI.TuringRigidity.ElementaryModel.globalGraph_inverse_pair line 79
9. theorem OAI.TuringRigidity.ElementaryModel.image_degreeSet_mem_hull line 92