OAI/Computability/DegreeRigidity/Effective/FiniteCodeBound.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.TuringRigidity.BoundedSetTheory.FiniteTuple.FiniteCode line 11
2. theorem OAI.TuringRigidity.BoundedSetTheory.FiniteTuple.FiniteCode.orderedPair line 16
3. theorem OAI.TuringRigidity.BoundedSetTheory.FiniteTuple.FiniteCode.mem_model line 21
4. theorem OAI.TuringRigidity.BoundedSetTheory.FiniteTuple.transitive_union line 28
5. theorem OAI.TuringRigidity.BoundedSetTheory.FiniteTuple.transitive_adjoin line 35
6. theorem OAI.TuringRigidity.BoundedSetTheory.FiniteTuple.FiniteCode.finite_transitive_extension line 43
7. theorem OAI.TuringRigidity.BoundedSetTheory.FiniteTuple.internal_finite_code_bound line 93