Theorems · Theorem · logic and foundations
Turing.PartrecToTM2.ret_supports
∀ {S : Finset Turing.PartrecToTM2.Λ'} {k : Turing.PartrecToTM2.Cont'},
Turing.PartrecToTM2.contSupp k ⊆ S → Turing.TM2.SupportsStmt S (Turing.PartrecToTM2.tr (Turing.PartrecToTM2.Λ'.ret k))- Cited by
- 2 results in Mathlib
- Foundations
- Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites26
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement and proof · cited by 13,712
- Turing.PartrecToTM2.Λ'statement and proof · cited by 85
- Turing.ToPartrec.Codeproof · cited by 83
- Turing.PartrecToTM2.Γ'statement and proof · cited by 83
- Turing.PartrecToTM2.K'statement · cited by 55
- Turing.PartrecToTM2.Cont'statement and proof · cited by 51
- Finset.mem_singleton_selfproof · cited by 44
- Turing.PartrecToTM2.trstatement · cited by 33
- Turing.PartrecToTM2.trNormalproof · cited by 23
- Turing.PartrecToTM2.trStmts₁proof · cited by 23
- Turing.PartrecToTM2.natEndproof · cited by 18
- Turing.PartrecToTM2.contSuppstatement and proof · cited by 18
Cited by2
Results whose statement or proof uses this declaration.
- Turing.PartrecToTM2.trStmts₁_supportsproof · cited by 2
- Turing.PartrecToTM2.codeSupp'_supportsproof · cited by 2