OAI/Computability/DegreeRigidity/SetModels/FiniteOrdinalCode.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TuringRigidity.OrdinalCoding.vectorCode line 8
  2. def OAI.TuringRigidity.OrdinalCoding.vectorDecode line 12
  3. theorem OAI.TuringRigidity.OrdinalCoding.vectorDecode_vectorCode line 17
  4. theorem OAI.TuringRigidity.OrdinalCoding.vectorCode_injective line 28
  5. theorem OAI.TuringRigidity.OrdinalCoding.entry_lt_vectorCode line 34
  6. theorem OAI.TuringRigidity.OrdinalCoding.vectorCode_pos line 43
  7. def OAI.TuringRigidity.OrdinalCoding.paddedCode line 48
  8. def OAI.TuringRigidity.OrdinalCoding.paddedDecode line 51
  9. theorem OAI.TuringRigidity.OrdinalCoding.paddedDecode_paddedCode line 54
  10. theorem OAI.TuringRigidity.OrdinalCoding.padding_recovered line 58
  11. theorem OAI.TuringRigidity.OrdinalCoding.padding_lt_paddedCode line 62
  12. theorem OAI.TuringRigidity.OrdinalCoding.entry_lt_paddedCode line 65
  13. theorem OAI.TuringRigidity.OrdinalCoding.paddedCode_inj line 68
  14. theorem OAI.TuringRigidity.OrdinalCoding.paddedCode_cofinal line 73
  15. theorem OAI.TuringRigidity.OrdinalCoding.pairCode_isSuccLimit line 78
  16. theorem OAI.TuringRigidity.OrdinalCoding.paddedCode_isSuccLimit line 87
  17. theorem OAI.TuringRigidity.OrdinalCoding.finite_margin_lt_paddedCode line 91