OAI/Computability/DegreeRigidity/Representation/BorelGeneric.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TuringRigidity.BorelGeneric.word line 8
2. theorem OAI.TuringRigidity.BorelGeneric.word_surjective line 10
3. def OAI.TuringRigidity.BorelGeneric.Ext line 14
4. def OAI.TuringRigidity.BorelGeneric.next line 20
5. theorem OAI.TuringRigidity.BorelGeneric.next_spec line 24
6. theorem OAI.TuringRigidity.BorelGeneric.next_measurable line 29
7. def OAI.TuringRigidity.BorelGeneric.stage line 36
8. theorem OAI.TuringRigidity.BorelGeneric.stage_measurable line 40
9. theorem OAI.TuringRigidity.BorelGeneric.stage_prefix line 48
10. theorem OAI.TuringRigidity.BorelGeneric.stage_length line 53
11. theorem OAI.TuringRigidity.BorelGeneric.stage_prefix_of_le line 62
12. def OAI.TuringRigidity.BorelGeneric.generic line 68
13. theorem OAI.TuringRigidity.BorelGeneric.generic_measurable line 71
14. def OAI.TuringRigidity.BorelGeneric.Meets line 78
15. theorem OAI.TuringRigidity.BorelGeneric.getD_prefix line 81
16. theorem OAI.TuringRigidity.BorelGeneric.meets_stage line 87
17. theorem OAI.TuringRigidity.BorelGeneric.borel_generic_selection line 98