OAI/Computability/DegreeRigidity/Constructibility/UniformSigmaDefinability.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TuringRigidity.BoundedDefinability.UniformSigmaDefinable line 9
2. theorem OAI.TuringRigidity.BoundedDefinability.Definable.toUniformSigma line 17
3. theorem OAI.TuringRigidity.BoundedDefinability.UniformSigmaDefinable.existsSet line 25
4. theorem OAI.TuringRigidity.BoundedDefinability.UniformSigmaDefinable.congr line 37
5. theorem OAI.TuringRigidity.BoundedDefinability.UniformSigmaDefinable.subst line 44
6. theorem OAI.TuringRigidity.BoundedDefinability.UniformSigmaDefinable.and line 54
7. theorem OAI.TuringRigidity.BoundedDefinability.UniformSigmaDefinable.or line 71
8. theorem OAI.TuringRigidity.BoundedDefinability.UniformSigmaDefinable.impBounded line 88
9. theorem OAI.TuringRigidity.BoundedDefinability.UniformSigmaDefinable.allMem line 96