OAI/Computability/DegreeRigidity/SetModels/ChoiceFromOrdinalCover.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TuringRigidity.BoundedSetTheory.InternalWellOrder.LeastValue line 11
2. theorem OAI.TuringRigidity.BoundedSetTheory.InternalWellOrder.leastValue_exists line 15
3. theorem OAI.TuringRigidity.BoundedSetTheory.InternalWellOrder.LeastValue.unique line 33
4. def OAI.TuringRigidity.BoundedSetTheory.InternalWellOrder.leastValueFormula line 47
5. theorem OAI.TuringRigidity.BoundedSetTheory.InternalWellOrder.eval_leastValueFormula line 53
6. def OAI.TuringRigidity.BoundedSetTheory.InternalWellOrder.selectionFormula line 58
7. theorem OAI.TuringRigidity.BoundedSetTheory.InternalWellOrder.internal_choice_of_ordinal_cover line 61