OAI/Computability/DegreeRigidity/SetModels/InternalMinimalSelector.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TuringRigidity.BoundedSetTheory.InternalWellOrder.MinimalIn line 11
2. def OAI.TuringRigidity.BoundedSetTheory.InternalWellOrder.InternallyWellFounded line 13
3. def OAI.TuringRigidity.BoundedSetTheory.InternalWellOrder.LeastMinimal line 16
4. theorem OAI.TuringRigidity.BoundedSetTheory.InternalWellOrder.leastMinimal_exists line 20
5. theorem OAI.TuringRigidity.BoundedSetTheory.InternalWellOrder.LeastMinimal.unique line 38
6. def OAI.TuringRigidity.BoundedSetTheory.InternalWellOrder.minimalInFormula line 50
7. theorem OAI.TuringRigidity.BoundedSetTheory.InternalWellOrder.eval_minimalInFormula line 53
8. def OAI.TuringRigidity.BoundedSetTheory.InternalWellOrder.leastMinimalFormula line 57
9. theorem OAI.TuringRigidity.BoundedSetTheory.InternalWellOrder.eval_leastMinimalFormula line 62
10. def OAI.TuringRigidity.BoundedSetTheory.InternalWellOrder.minimalSelectorFormula line 67
11. theorem OAI.TuringRigidity.BoundedSetTheory.InternalWellOrder.internal_minimal_selector line 70