OAI/Computability/DegreeRigidity/Constructibility/RelativeModelClosure.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TuringRigidity.RelativeConstructible.finite_parameters_in_relative_level line 10
2. theorem OAI.TuringRigidity.RelativeConstructible.empty_in_relativeModel line 24
3. theorem OAI.TuringRigidity.RelativeConstructible.pair_in_relativeModel line 30
4. theorem OAI.TuringRigidity.RelativeConstructible.union_in_relativeModel line 41
5. theorem OAI.TuringRigidity.RelativeConstructible.bounded_separation_in_relativeModel line 49
6. theorem OAI.TuringRigidity.RelativeConstructible.relativeModel_pairing line 80
7. theorem OAI.TuringRigidity.RelativeConstructible.relativeModel_union line 88
8. theorem OAI.TuringRigidity.RelativeConstructible.relativeModel_bounded_separation line 100
9. theorem OAI.TuringRigidity.RelativeConstructible.ground_relativeModel_omega line 111
10. theorem OAI.TuringRigidity.RelativeConstructible.ground_relativeModel_infinity line 116