OAI/Computability/DegreeRigidity/SetModels/SkolemHull.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TuringRigidity.BoundedSetTheory.FiniteTuple.hull line 11
2. theorem OAI.TuringRigidity.BoundedSetTheory.FiniteTuple.mem_hull line 14
3. def OAI.TuringRigidity.BoundedSetTheory.FiniteTuple.hullFormula line 17
4. theorem OAI.TuringRigidity.BoundedSetTheory.FiniteTuple.hull_mem line 20
5. theorem OAI.TuringRigidity.BoundedSetTheory.FiniteTuple.hull_subset line 50
6. theorem OAI.TuringRigidity.BoundedSetTheory.FiniteTuple.seed_subset_hull line 53
7. theorem OAI.TuringRigidity.BoundedSetTheory.FiniteTuple.hull_closed line 57
8. theorem OAI.TuringRigidity.BoundedSetTheory.FiniteTuple.hull_least line 68
9. theorem OAI.TuringRigidity.BoundedSetTheory.FiniteTuple.internal_finite_hull line 72