OAI/Computability/DegreeRigidity/SetModels/ModelReals.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TuringRigidity.BoundedSetTheory.realCode line 11
2. theorem OAI.TuringRigidity.BoundedSetTheory.realCode_subset line 14
3. theorem OAI.TuringRigidity.BoundedSetTheory.natSet_mem_realCode line 17
4. def OAI.TuringRigidity.BoundedSetTheory.decodeReal line 26
5. theorem OAI.TuringRigidity.BoundedSetTheory.decodeReal_true line 30
6. theorem OAI.TuringRigidity.BoundedSetTheory.realCode_decodeReal line 34
7. theorem OAI.TuringRigidity.BoundedSetTheory.realCode_injective line 41
8. theorem OAI.TuringRigidity.BoundedSetTheory.decodeReal_realCode line 48
9. def OAI.TuringRigidity.BoundedSetTheory.modelReals line 51
10. theorem OAI.TuringRigidity.BoundedSetTheory.internal_real_power line 53