Theorems · Definition · combinatorics
Finset.restrict
{ι : Type u_2} → {π : ι → Type u_3} → (s : Finset ι) → ((i : ι) → π i) → (i : ↥s) → π ↑iRestrict domain of a function f to a finite set s.
- Defined in
- Mathlib.Data.Finset.Pi
- Cited by
- 60 results in Mathlib
- Foundations
- Depth 54 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
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
Cited by68
Results whose statement or proof uses this declaration.
- MeasureTheory.cylinderproof · cited by 49
- Preorder.frestrictLeproof · cited by 43
- Finset.measurable_restrictstatement and proof · cited by 17
- MeasureTheory.IsProjectiveLimitproof · cited by 13
- ProbabilityTheory.IsGaussianProcess.hasGaussianLawstatement · cited by 10
- ProbabilityTheory.IsPreBrownianReal.covariance_evalproof · cited by 5
- ProbabilityTheory.IsPreBrownianReal.hasLawstatement · cited by 5
- MeasureTheory.Filtration.piFinsetproof · cited by 5
- ProbabilityTheory.iIndepFun.restrictstatement · cited by 5
- MeasureTheory.Measure.infinitePi_map_restrictstatement · cited by 5
- Finset.restrict₂_comp_restrictstatement · cited by 4
- ProbabilityTheory.iIndepFun.charFunDual_map_finsetSum_eq_prodstatement and proof · cited by 4