OAI/Computability/DegreeRigidity/SetModels/TransitiveNameModel.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.TuringRigidity.TransitiveNameModel.Conditions line 10
  2. def OAI.TuringRigidity.TransitiveNameModel.label line 12
  3. theorem OAI.TuringRigidity.TransitiveNameModel.label_injective line 15
  4. theorem OAI.TuringRigidity.TransitiveNameModel.label_mem line 18
  5. def OAI.TuringRigidity.TransitiveNameModel.names line 21
  6. def OAI.TuringRigidity.TransitiveNameModel.Transitive line 24
  7. def OAI.TuringRigidity.TransitiveNameModel.genericExtension line 26
  8. theorem OAI.TuringRigidity.TransitiveNameModel.names_childClosed line 29
  9. theorem OAI.TuringRigidity.TransitiveNameModel.genericExtension_transitive line 42
  10. def OAI.TuringRigidity.TransitiveNameModel.valueOnCode line 47
  11. theorem OAI.TuringRigidity.TransitiveNameModel.valueOnCode_encode line 53
  12. theorem OAI.TuringRigidity.TransitiveNameModel.genericExtension_countable line 62
  13. def OAI.TuringRigidity.TransitiveNameModel.genericExtensionSet line 69
  14. theorem OAI.TuringRigidity.TransitiveNameModel.genericExtensionSet_coe line 74
  15. theorem OAI.TuringRigidity.TransitiveNameModel.genericExtensionSet_transitive line 90
  16. theorem OAI.TuringRigidity.TransitiveNameModel.ground_subset line 99