OAI/Computability/DegreeRigidity/SetModels/RegularCompletion.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.TuringRigidity.RegularCompletion.Algebra line 12
  2. instance OAI.TuringRigidity.RegularCompletion.algebraCompleteBoolean line 14
  3. def OAI.TuringRigidity.RegularCompletion.basic line 21
  4. theorem OAI.TuringRigidity.RegularCompletion.basic_le_iff line 23
  5. theorem OAI.TuringRigidity.RegularCompletion.mem_basic line 26
  6. theorem OAI.TuringRigidity.RegularCompletion.basic_nonzero line 29
  7. theorem OAI.TuringRigidity.RegularCompletion.basic_mono line 35
  8. theorem OAI.TuringRigidity.RegularCompletion.mem_compl line 39
  9. theorem OAI.TuringRigidity.RegularCompletion.mem_basic_iff line 52
  10. theorem OAI.TuringRigidity.RegularCompletion.basic_dense line 60
  11. theorem OAI.TuringRigidity.RegularCompletion.refine_basic line 72
  12. def OAI.TuringRigidity.RegularCompletion.positiveBasic line 79
  13. theorem OAI.TuringRigidity.RegularCompletion.positiveBasic_dense line 82
  14. theorem OAI.TuringRigidity.RegularCompletion.positiveBasic_countable line 87