OAI/Computability/DegreeRigidity/SetModels/NameExtension.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TuringRigidity.RecursiveNames.Name.Child line 11
  2. def OAI.TuringRigidity.RecursiveNames.extension line 14
  3. def OAI.TuringRigidity.RecursiveNames.ChildClosed line 16
  4. theorem OAI.TuringRigidity.RecursiveNames.extension_transitive line 19
  5. theorem OAI.TuringRigidity.RecursiveNames.extension_countable line 27
  6. theorem OAI.TuringRigidity.RecursiveNames.ground_subset_extension line 30
  7. def OAI.TuringRigidity.RecursiveNames.Name.pair line 36
  8. theorem OAI.TuringRigidity.RecursiveNames.Name.val_pair line 39
  9. def OAI.TuringRigidity.RecursiveNames.Name.arity line 53
  10. def OAI.TuringRigidity.RecursiveNames.Name.child line 56
  11. def OAI.TuringRigidity.RecursiveNames.Name.tag line 59
  12. def OAI.TuringRigidity.RecursiveNames.Name.union line 62
  13. theorem OAI.TuringRigidity.RecursiveNames.Name.mem_val_children line 67
  14. theorem OAI.TuringRigidity.RecursiveNames.Name.val_union line 72
  15. theorem OAI.TuringRigidity.RecursiveNames.extension_pair_closed line 90