OAI/Computability/DegreeRigidity/SetModels/ChoiceTrace.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TuringRigidity.BoundedSetTheory.InternalWellOrder.Remaining line 13
2. structure OAI.TuringRigidity.BoundedSetTheory.InternalWellOrder.Trace line 16
3. theorem OAI.TuringRigidity.BoundedSetTheory.InternalWellOrder.Trace.pair_mem line 23
4. theorem OAI.TuringRigidity.BoundedSetTheory.InternalWellOrder.choice_value_mem line 29
5. theorem OAI.TuringRigidity.BoundedSetTheory.InternalWellOrder.Remaining.eq line 35
6. theorem OAI.TuringRigidity.BoundedSetTheory.InternalWellOrder.Trace.compatible line 51
7. theorem OAI.TuringRigidity.BoundedSetTheory.InternalWellOrder.Trace.functional line 75
8. theorem OAI.TuringRigidity.BoundedSetTheory.InternalWellOrder.Trace.injective line 79
9. theorem OAI.TuringRigidity.BoundedSetTheory.InternalWellOrder.Trace.sUnion line 92