OAI/Computability/DegreeRigidity/Representation/NativeModelCompatibility.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.TuringRigidity.BoundedSetTheory.realCode_eq_realSetline 11 - theorem
OAI.TuringRigidity.BoundedSetTheory.modelReals_eq_realsline 13 - theorem
OAI.TuringRigidity.BoundedSetTheory.native_countability_iffline 15 - theorem
OAI.TuringRigidity.BoundedSetTheory.degreeCode_eq_degreeSetline 29 - theorem
OAI.TuringRigidity.BoundedSetTheory.presentationSet_eq_idealSetline 41 - theorem
OAI.TuringRigidity.BoundedSetTheory.presentationGraph_eq_automorphismSetline 55