OAI/Computability/DegreeRigidity/Syntax/DefinablePower.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TuringRigidity.RelativeConstructible.tupleEnv line 10
  2. theorem OAI.TuringRigidity.RelativeConstructible.tupleEnv_lt line 13
  3. def OAI.TuringRigidity.RelativeConstructible.definedSubset line 16
  4. theorem OAI.TuringRigidity.RelativeConstructible.mem_definedSubset line 20
  5. def OAI.TuringRigidity.RelativeConstructible.DefinableOver line 25
  6. def OAI.TuringRigidity.RelativeConstructible.definablePower line 29
  7. theorem OAI.TuringRigidity.RelativeConstructible.definableOver_subset line 32
  8. theorem OAI.TuringRigidity.RelativeConstructible.mem_definablePower line 36
  9. theorem OAI.TuringRigidity.RelativeConstructible.subset_of_mem_definablePower line 41
  10. theorem OAI.TuringRigidity.RelativeConstructible.separation_mem_definablePower line 45
  11. theorem OAI.TuringRigidity.RelativeConstructible.self_mem_definablePower line 62
  12. theorem OAI.TuringRigidity.RelativeConstructible.subset_definablePower line 68
  13. theorem OAI.TuringRigidity.RelativeConstructible.definablePower_transitive line 77