OAI/Computability/DegreeRigidity/SetModels/ChoiceTraceFormula.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TuringRigidity.BoundedSetTheory.InternalWellOrder.remainingFormula line 12
2. theorem OAI.TuringRigidity.BoundedSetTheory.InternalWellOrder.eval_remainingFormula line 16
3. def OAI.TuringRigidity.BoundedSetTheory.InternalWellOrder.traceFormula line 21
4. theorem OAI.TuringRigidity.BoundedSetTheory.InternalWellOrder.eval_traceFormula line 29
5. theorem OAI.TuringRigidity.BoundedSetTheory.InternalWellOrder.Trace.subset line 36
6. theorem OAI.TuringRigidity.BoundedSetTheory.InternalWellOrder.internal_maximal_trace line 39
7. def OAI.TuringRigidity.BoundedSetTheory.InternalWellOrder.residual line 63
8. theorem OAI.TuringRigidity.BoundedSetTheory.InternalWellOrder.residual_remaining line 66
9. theorem OAI.TuringRigidity.BoundedSetTheory.InternalWellOrder.residual_mem line 71