OAI/Computability/DegreeRigidity/SetModels/IdealLift.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TuringRigidity.IdealInterpretation.ACode.ofBelow line 9
2. theorem OAI.TuringRigidity.IdealInterpretation.ACode.external_ofBelow line 13
3. def OAI.TuringRigidity.IdealInterpretation.SCode.ofBelow line 16
4. theorem OAI.TuringRigidity.IdealInterpretation.SCode.external_ofBelow line 19
5. def OAI.TuringRigidity.IdealInterpretation.RCode.ofBelow line 22
6. theorem OAI.TuringRigidity.IdealInterpretation.RCode.external_ofBelow line 26
7. theorem OAI.TuringRigidity.IdealInterpretation.ACode.map_below line 29
8. theorem OAI.TuringRigidity.IdealInterpretation.SCode.map_below line 35
9. theorem OAI.TuringRigidity.IdealInterpretation.RCode.map_below line 40
10. theorem OAI.TuringRigidity.IdealInterpretation.RCode.coordinates_mem line 44
11. theorem OAI.TuringRigidity.IdealInterpretation.RCode.transport_one line 49
12. theorem OAI.TuringRigidity.IdealInterpretation.RCode.transport_two line 57