OAI/Computability/DegreeRigidity/Constructibility/ConstructibleStages.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TuringRigidity.RelativeConstructible.stage line 11
  2. theorem OAI.TuringRigidity.RelativeConstructible.mem_stage line 17
  3. theorem OAI.TuringRigidity.RelativeConstructible.seed_subset_stage line 29
  4. theorem OAI.TuringRigidity.RelativeConstructible.stage_zero line 32
  5. theorem OAI.TuringRigidity.RelativeConstructible.stage_transitive line 36
  6. theorem OAI.TuringRigidity.RelativeConstructible.stage_mono line 44
  7. theorem OAI.TuringRigidity.RelativeConstructible.definablePower_subset_stage line 50
  8. theorem OAI.TuringRigidity.RelativeConstructible.stage_mem_stage line 54
  9. theorem OAI.TuringRigidity.RelativeConstructible.stage_succ line 58
  10. def OAI.TuringRigidity.RelativeConstructible.level line 70
  11. theorem OAI.TuringRigidity.RelativeConstructible.level_zero line 72
  12. theorem OAI.TuringRigidity.RelativeConstructible.level_succ line 75
  13. theorem OAI.TuringRigidity.RelativeConstructible.level_mono line 79
  14. theorem OAI.TuringRigidity.RelativeConstructible.level_mem_level line 82
  15. theorem OAI.TuringRigidity.RelativeConstructible.level_transitive line 85
  16. theorem OAI.TuringRigidity.RelativeConstructible.mem_level_limit line 88
  17. def OAI.TuringRigidity.RelativeConstructible.InRelativeL line 101
  18. theorem OAI.TuringRigidity.RelativeConstructible.parameter_in_relativeL line 103
  19. theorem OAI.TuringRigidity.RelativeConstructible.relativeL_transitive line 106