OAI/Computability/DegreeRigidity/Representation/SourceTDependentChoice.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TuringRigidity.BoundedSetTheory.sourceT_dependent_choice line 12
2. theorem OAI.TuringRigidity.BoundedSetTheory.sourceT_internal_descent line 33
3. theorem OAI.TuringRigidity.BoundedSetTheory.wellFounded_no_descent line 51
4. theorem OAI.TuringRigidity.BoundedSetTheory.sourceT_descent_absolute line 62