OAI/Computability/DegreeRigidity/CohenForcing/CohenRecursiveName.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.TuringRigidity.CohenRecursiveName.(instance at line 9) line 9
2. def OAI.TuringRigidity.CohenRecursiveName.numeral line 13
3. def OAI.TuringRigidity.CohenRecursiveName.realSet line 15
4. theorem OAI.TuringRigidity.CohenRecursiveName.numeral_mem_omega line 18
5. theorem OAI.TuringRigidity.CohenRecursiveName.realSet_subset_omega line 22
6. def OAI.TuringRigidity.CohenRecursiveName.genericReal line 27
7. theorem OAI.TuringRigidity.CohenRecursiveName.val_genericReal line 31
8. theorem OAI.TuringRigidity.CohenRecursiveName.genericReal_from_filter line 51
9. theorem OAI.TuringRigidity.CohenRecursiveName.exists_generic_real line 57