Theorems · Inductive type · real analysis
OrderedFinpartition
ℕ → Type
A partition of Fin n into finitely many nonempty subsets, given by the increasing
parameterization of these subsets. We order the subsets by increasing greatest element.
This definition is tailored-made for the Faa di Bruno formula, and probably not useful elsewhere,
because of the specific parameterization by Fin n and the peculiar ordering.
- Cited by
- 61 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by87
Results whose statement or proof uses this declaration.
- OrderedFinpartition.lengthstatement and proof · cited by 54
- OrderedFinpartition.partSizestatement and proof · cited by 47
- OrderedFinpartition.embstatement and proof · cited by 26
- FormalMultilinearSeries.taylorCompproof · cited by 9
- OrderedFinpartition.applyOrderedFinpartitionstatement and proof · cited by 8
- OrderedFinpartition.atomicstatement · cited by 7
- OrderedFinpartition.compAlongOrderedFinpartitionLstatement and proof · cited by 6
- OrderedFinpartition.emb_strictMonostatement and proof · cited by 6
- OrderedFinpartition.extendMiddlestatement and proof · cited by 6
- OrderedFinpartition.indexstatement and proof · cited by 6
- OrderedFinpartition.compAlongOrderedFinpartitionstatement and proof · cited by 5
- OrderedFinpartition.extendstatement and proof · cited by 5