OAI/Computability/DegreeRigidity/Constructibility/RelativeModel.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TuringRigidity.RelativeConstructible.InRelativeModel line 10
  2. def OAI.TuringRigidity.RelativeConstructible.relativeModel line 13
  3. theorem OAI.TuringRigidity.RelativeConstructible.relativeModel_subset line 16
  4. theorem OAI.TuringRigidity.RelativeConstructible.InRelativeModel.mem_ground line 19
  5. theorem OAI.TuringRigidity.RelativeConstructible.mem_relativeModel line 25
  6. theorem OAI.TuringRigidity.RelativeConstructible.InRelativeModel.external line 31
  7. theorem OAI.TuringRigidity.RelativeConstructible.InRelativeModel.transitive line 36
  8. theorem OAI.TuringRigidity.RelativeConstructible.relativeModel_transitive line 41
  9. theorem OAI.TuringRigidity.RelativeConstructible.internal_ordinal_zero line 47
  10. theorem OAI.TuringRigidity.RelativeConstructible.internal_ordinal_succ line 52
  11. theorem OAI.TuringRigidity.RelativeConstructible.internal_ordinal_max line 62
  12. theorem OAI.TuringRigidity.RelativeConstructible.parameter_in_relativeModel line 68
  13. theorem OAI.TuringRigidity.RelativeConstructible.level_in_relativeModel line 72
  14. theorem OAI.TuringRigidity.RelativeConstructible.relativeModel_ground_reals line 78
  15. theorem OAI.TuringRigidity.RelativeConstructible.relativeModel_monotone line 84
  16. theorem OAI.TuringRigidity.RelativeConstructible.relativeModel_external line 90