OAI/Computability/DegreeRigidity/Constructibility/ContextDefinablePower.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TuringRigidity.RelativeConstructible.tupleSpace_mem_of_context line 10
2. theorem OAI.TuringRigidity.RelativeConstructible.truthSlice_mem_of_context line 35
3. theorem OAI.TuringRigidity.RelativeConstructible.finiteSatisfaction_mem_of_context line 62
4. theorem OAI.TuringRigidity.RelativeConstructible.internal_certificate_bound_of_context line 71
5. theorem OAI.TuringRigidity.RelativeConstructible.satisfactionSet_mem_of_context line 81
6. theorem OAI.TuringRigidity.RelativeConstructible.definablePower_mem_of_context line 102
7. theorem OAI.TuringRigidity.RelativeConstructible.internal_defSystem_of_context line 125