OAI/Computability/DegreeRigidity/Constructibility/RelativeConstruction.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.TuringRigidity.RelativeConstructible.Construction line 11
2. def OAI.TuringRigidity.RelativeConstructible.Construction.value line 17
3. def OAI.TuringRigidity.RelativeConstructible.Construction.Certified line 23
4. def OAI.TuringRigidity.RelativeConstructible.Construction.Indexed line 29
5. theorem OAI.TuringRigidity.RelativeConstructible.Construction.value_in_relativeL line 34
6. theorem OAI.TuringRigidity.RelativeConstructible.Construction.value_in_relativeModel line 44
7. theorem OAI.TuringRigidity.RelativeConstructible.ground_seed_shape line 55
8. theorem OAI.TuringRigidity.RelativeConstructible.construction_of_level line 74
9. theorem OAI.TuringRigidity.RelativeConstructible.construction_of_relativeModel line 107