OAI/Computability/DegreeRigidity/SetModels/RelationHull.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TuringRigidity.RelationHull.Closed line 10
  2. def OAI.TuringRigidity.RelationHull.Code.closed line 16
  3. theorem OAI.TuringRigidity.RelationHull.Code.eval_closed line 19
  4. def OAI.TuringRigidity.RelationHull.Code.member line 23
  5. theorem OAI.TuringRigidity.RelationHull.Code.eval_member line 26
  6. def OAI.TuringRigidity.RelationHull.Code.isHull line 32
  7. theorem OAI.TuringRigidity.RelationHull.Code.eval_isHull line 36
  8. def OAI.TuringRigidity.RelationHull.hull line 43
  9. theorem OAI.TuringRigidity.RelationHull.mem_hull line 46
  10. theorem OAI.TuringRigidity.RelationHull.hull_subset line 49
  11. theorem OAI.TuringRigidity.RelationHull.self_mem line 52
  12. theorem OAI.TuringRigidity.RelationHull.hull_closed line 55
  13. theorem OAI.TuringRigidity.RelationHull.hull_least line 60
  14. theorem OAI.TuringRigidity.RelationHull.hull_mem line 64
  15. theorem OAI.TuringRigidity.RelationHull.isHull_iff line 82
  16. def OAI.TuringRigidity.RelationHull.predecessors line 99
  17. theorem OAI.TuringRigidity.RelationHull.mem_predecessors line 102
  18. theorem OAI.TuringRigidity.RelationHull.predecessors_mem line 105
  19. theorem OAI.TuringRigidity.RelationHull.collect_hulls line 112
  20. theorem OAI.TuringRigidity.RelationHull.hull_unfold line 134