OAI/Computability/DegreeRigidity/Constructibility/PersistentRestrictions.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.TuringRigidity.PersistentRestrictions.countable_principal_lower line 8
  2. structure OAI.TuringRigidity.PersistentRestrictions.CountableIdeal line 15
  3. instance OAI.TuringRigidity.PersistentRestrictions.(instance at line 22) line 22
  4. def OAI.TuringRigidity.PersistentRestrictions.closureStep line 24
  5. theorem OAI.TuringRigidity.PersistentRestrictions.countable_closureStep line 28
  6. def OAI.TuringRigidity.PersistentRestrictions.stage line 33
  7. theorem OAI.TuringRigidity.PersistentRestrictions.countable_stage line 37
  8. theorem OAI.TuringRigidity.PersistentRestrictions.stage_mono line 42
  9. def OAI.TuringRigidity.PersistentRestrictions.hullSet line 47
  10. theorem OAI.TuringRigidity.PersistentRestrictions.subset_hullSet line 49
  11. theorem OAI.TuringRigidity.PersistentRestrictions.hullSet_lower line 53
  12. theorem OAI.TuringRigidity.PersistentRestrictions.hullSet_join line 60
  13. theorem OAI.TuringRigidity.PersistentRestrictions.hullSet_forward line 70
  14. theorem OAI.TuringRigidity.PersistentRestrictions.hullSet_backward line 75
  15. def OAI.TuringRigidity.PersistentRestrictions.invariantHull line 80
  16. theorem OAI.TuringRigidity.PersistentRestrictions.countable_invariant_hull line 88
  17. def OAI.TuringRigidity.PersistentRestrictions.restrict line 95
  18. def OAI.TuringRigidity.PersistentRestrictions.Extends line 104
  19. def OAI.TuringRigidity.PersistentRestrictions.Persistent line 108
  20. def OAI.TuringRigidity.PersistentRestrictions.RestrictsTo line 112
  21. theorem OAI.TuringRigidity.PersistentRestrictions.persistent_of_global_restriction line 115
  22. theorem OAI.TuringRigidity.PersistentRestrictions.global_restriction_set_extension line 125
  23. theorem OAI.TuringRigidity.PersistentRestrictions.persistent_countable_extension line 133
  24. theorem OAI.TuringRigidity.PersistentRestrictions.nontrivial_persistent_restriction line 145
  25. theorem OAI.TuringRigidity.PersistentRestrictions.nonrigidity_has_nontrivial_persistent line 157