OAI/Computability/DegreeRigidity/SetModels/InternalHull.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TuringRigidity.BoundedSetTheory.hull line 9
  2. theorem OAI.TuringRigidity.BoundedSetTheory.mem_hull line 12
  3. def OAI.TuringRigidity.BoundedSetTheory.hullMemberFormula line 16
  4. theorem OAI.TuringRigidity.BoundedSetTheory.eval_hullMemberFormula line 19
  5. theorem OAI.TuringRigidity.BoundedSetTheory.hull_mem line 26
  6. theorem OAI.TuringRigidity.BoundedSetTheory.hull_subset line 41
  7. theorem OAI.TuringRigidity.BoundedSetTheory.self_mem_hull line 44
  8. theorem OAI.TuringRigidity.BoundedSetTheory.hull_transitive line 47
  9. theorem OAI.TuringRigidity.BoundedSetTheory.hull_least line 54
  10. def OAI.TuringRigidity.BoundedSetTheory.Formula.isHull line 59
  11. theorem OAI.TuringRigidity.BoundedSetTheory.Formula.eval_isHull line 63
  12. theorem OAI.TuringRigidity.BoundedSetTheory.isHull_iff line 71
  13. theorem OAI.TuringRigidity.BoundedSetTheory.collect_hulls line 89
  14. theorem OAI.TuringRigidity.BoundedSetTheory.hull_unfold line 114