Theorems · Theorem · logic and foundations
Turing.TM1to0.tr_supports
∀ {Γ : Type u_1} {Λ : Type u_2} [inst : Inhabited Λ] {σ : Type u_3} [inst_1 : Inhabited σ]
(M : Λ → Turing.TM1.Stmt Γ Λ σ) [inst_2 : Fintype σ] {S : Finset Λ},
Turing.TM1.Supports M S → Turing.TM0.Supports (Turing.TM1to0.tr M) ↑(Turing.TM1to0.trStmts M S)- Cited by
- 0 results in Mathlib
- Foundations
- Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites31
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
- SetLike.coestatement and proof · cited by 8,199
- Fintypestatement and proof · cited by 7,736
- Finset.mapproof · cited by 747
- Finset.valproof · cited by 438
- Finset.mem_univproof · cited by 361
- Finset.biUnionproof · cited by 217
- Finset.mem_insert_of_memproof · cited by 109
- Turing.TM1.Stmtstatement and proof · cited by 49
- Finset.mem_productproof · cited by 48
- Multiset.mem_cons_selfproof · cited by 44
- Function.Embedding.someproof · cited by 43
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.