OAI/Computability/DegreeRigidity/SetModels/InternalRegularOperations.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TuringRigidity.InternalRegularOperations.neg line 10
  2. def OAI.TuringRigidity.InternalRegularOperations.regular line 13
  3. def OAI.TuringRigidity.InternalRegularOperations.Lower line 15
  4. theorem OAI.TuringRigidity.InternalRegularOperations.neg_subset line 18
  5. theorem OAI.TuringRigidity.InternalRegularOperations.neg_lower line 21
  6. theorem OAI.TuringRigidity.InternalRegularOperations.neg_mem line 27
  7. theorem OAI.TuringRigidity.InternalRegularOperations.regular_mem line 34
  8. def OAI.TuringRigidity.InternalRegularOperations.decode line 38
  9. theorem OAI.TuringRigidity.InternalRegularOperations.decode_injective line 44
  10. theorem OAI.TuringRigidity.InternalRegularOperations.decode_neg line 60
  11. theorem OAI.TuringRigidity.InternalRegularOperations.decode_regular line 76
  12. theorem OAI.TuringRigidity.InternalRegularOperations.regular_idempotent line 83
  13. theorem OAI.TuringRigidity.InternalRegularOperations.neg_regular line 88
  14. theorem OAI.TuringRigidity.InternalRegularOperations.union_lower line 95
  15. def OAI.TuringRigidity.InternalRegularOperations.supCode line 101
  16. theorem OAI.TuringRigidity.InternalRegularOperations.join_mem line 103
  17. def OAI.TuringRigidity.InternalRegularOperations.bitCode line 107
  18. theorem OAI.TuringRigidity.InternalRegularOperations.bitCode_mem line 110