OAI/Computability/DegreeRigidity/SetModels/ElementaryDefinableSets.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.TuringRigidity.ElementaryModel.unique_definable_mem line 11
  2. theorem OAI.TuringRigidity.ElementaryModel.unorderedPair_mem_hull line 21
  3. theorem OAI.TuringRigidity.ElementaryModel.orderedPair_mem_hull line 29
  4. theorem OAI.TuringRigidity.ElementaryModel.collapse_unorderedPair line 35
  5. theorem OAI.TuringRigidity.ElementaryModel.collapse_orderedPair line 53
  6. def OAI.TuringRigidity.ElementaryModel.ambientRealSet line 63
  7. def OAI.TuringRigidity.ElementaryModel.ambientGraphBound line 64
  8. theorem OAI.TuringRigidity.ElementaryModel.ambient_real_decode line 66
  9. theorem OAI.TuringRigidity.ElementaryModel.ambient_graph_bound line 70
  10. theorem OAI.TuringRigidity.ElementaryModel.ambient_degreeCode line 77
  11. theorem OAI.TuringRigidity.ElementaryModel.degreeSet_mem_hull line 83