OAI/Computability/DegreeRigidity/Effective/ProgramTopology.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TuringRigidity.OpenFiber line 10
  2. theorem OAI.TuringRigidity.OpenFiber.const line 16
  3. theorem OAI.TuringRigidity.OpenFiber.map line 20
  4. theorem OAI.TuringRigidity.OpenFiber.bind line 34
  5. theorem OAI.TuringRigidity.OpenFiber.seq line 45
  6. theorem OAI.TuringRigidity.OpenFiber.some line 50
  7. theorem OAI.TuringRigidity.OpenFiber.rfind line 56
  8. theorem OAI.TuringRigidity.OracleCode.eval_openFiber line 74
  9. theorem OAI.TuringRigidity.OracleCode.halting_set_open line 100
  10. theorem OAI.TuringRigidity.OracleCode.eval_eq_oracle_iff line 108
  11. theorem OAI.TuringRigidity.OracleCode.success_measurable line 119