OAI/Computability/DegreeRigidity/OrdinalCodes/IndexPresentation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.TuringRigidity.IndexPresentation.Dom line 9
  2. def OAI.TuringRigidity.IndexPresentation.LE line 10
  3. def OAI.TuringRigidity.IndexPresentation.joinIndex line 11
  4. theorem OAI.TuringRigidity.IndexPresentation.joinIndex_primrec line 13
  5. def OAI.TuringRigidity.IndexPresentation.value line 17
  6. theorem OAI.TuringRigidity.IndexPresentation.value_eq line 21
  7. theorem OAI.TuringRigidity.IndexPresentation.value_below line 27
  8. theorem OAI.TuringRigidity.IndexPresentation.value_surjective line 34
  9. theorem OAI.TuringRigidity.IndexPresentation.le_iff line 41
  10. theorem OAI.TuringRigidity.IndexPresentation.join_dom line 47
  11. theorem OAI.TuringRigidity.IndexPresentation.join_value line 55