OAI/Computability/DegreeRigidity/SetModels/InternalRegularAlgebra.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TuringRigidity.InternalRegularAlgebra.IsCode line 9
  2. theorem OAI.TuringRigidity.InternalRegularAlgebra.mem_regular line 11
  3. theorem OAI.TuringRigidity.InternalRegularAlgebra.isCode_iff line 25
  4. def OAI.TuringRigidity.InternalRegularAlgebra.codeFormula line 38
  5. theorem OAI.TuringRigidity.InternalRegularAlgebra.codeFormula_spec line 42
  6. theorem OAI.TuringRigidity.InternalRegularAlgebra.internal_algebra line 48
  7. theorem OAI.TuringRigidity.InternalRegularAlgebra.code_lower line 61
  8. def OAI.TuringRigidity.InternalRegularAlgebra.interpret line 65
  9. theorem OAI.TuringRigidity.InternalRegularAlgebra.interpret_le_iff line 76
  10. theorem OAI.TuringRigidity.InternalRegularAlgebra.interpret_injective line 85
  11. theorem OAI.TuringRigidity.InternalRegularAlgebra.neg_isCode line 91
  12. theorem OAI.TuringRigidity.InternalRegularAlgebra.regular_isCode line 94
  13. theorem OAI.TuringRigidity.InternalRegularAlgebra.join_isCode line 97
  14. theorem OAI.TuringRigidity.InternalRegularAlgebra.interpret_neg line 99
  15. theorem OAI.TuringRigidity.InternalRegularAlgebra.internal_complement line 104
  16. theorem OAI.TuringRigidity.InternalRegularAlgebra.internal_join line 109