OAI/Computability/DegreeRigidity/SetModels/ExtensionBasicAxioms.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TuringRigidity.TransitiveNameModel.BasicAxioms.Extensionality line 11
  2. def OAI.TuringRigidity.TransitiveNameModel.BasicAxioms.EmptySet line 14
  3. def OAI.TuringRigidity.TransitiveNameModel.BasicAxioms.Foundation line 16
  4. theorem OAI.TuringRigidity.TransitiveNameModel.BasicAxioms.extensionality line 20
  5. theorem OAI.TuringRigidity.TransitiveNameModel.BasicAxioms.foundation line 27
  6. theorem OAI.TuringRigidity.TransitiveNameModel.empty_mem_ground line 37
  7. def OAI.TuringRigidity.TransitiveNameModel.emptyName line 50
  8. theorem OAI.TuringRigidity.TransitiveNameModel.encode_emptyName line 53
  9. theorem OAI.TuringRigidity.TransitiveNameModel.val_emptyName line 59
  10. theorem OAI.TuringRigidity.TransitiveNameModel.mem_extensionSet line 64
  11. theorem OAI.TuringRigidity.TransitiveNameModel.extension_empty_mem line 71
  12. theorem OAI.TuringRigidity.TransitiveNameModel.encode_pair line 78
  13. theorem OAI.TuringRigidity.TransitiveNameModel.names_pair_closed line 94
  14. theorem OAI.TuringRigidity.TransitiveNameModel.extension_pairing line 103
  15. theorem OAI.TuringRigidity.TransitiveNameModel.names_union_closed line 113
  16. theorem OAI.TuringRigidity.TransitiveNameModel.extension_union line 123
  17. theorem OAI.TuringRigidity.TransitiveNameModel.extension_five_axioms line 141