OAI/Computability/DegreeRigidity/SetModels/SetModelReals.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TuringRigidity.SetModelReals.realSet line 11
  2. theorem OAI.TuringRigidity.SetModelReals.nat_mem_realSet line 14
  3. theorem OAI.TuringRigidity.SetModelReals.realSet_subset line 23
  4. theorem OAI.TuringRigidity.SetModelReals.realSet_injective line 26
  5. def OAI.TuringRigidity.SetModelReals.oracleOf line 32
  6. theorem OAI.TuringRigidity.SetModelReals.oracleOf_realSet line 36
  7. theorem OAI.TuringRigidity.SetModelReals.realSet_oracleOf line 41
  8. def OAI.TuringRigidity.SetModelReals.reals line 54
  9. theorem OAI.TuringRigidity.SetModelReals.internal_reals line 56
  10. theorem OAI.TuringRigidity.SetModelReals.omega_exists line 69
  11. theorem OAI.TuringRigidity.SetModelReals.real_formula_absolute line 78
  12. theorem OAI.TuringRigidity.SetModelReals.real_comprehension line 82