Mathlib Map

Theorems · Theorem · combinatorics

Composition.sizeUpTo_index_le

∀ {n : ℕ} (c : Composition n) (j : Fin n), c.sizeUpTo ↑(c.index j) ≤ ↑j
Defined in
Mathlib.Combinatorics.Enumerative.Composition
Cited by
1 results in Mathlib
Foundations
Depth 26 from the axioms · uses propext
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Composition.embedding_comp_inv · cited by 2Composition.embedding_com…ne_of_gt · cited by 637ne_of_gtlt_trans · cited by 165lt_transComposition · cited by 138Compositionnonpos_iff_eq_zero · cited by 100nonpos_iff_eq_zeroComposition.length · cited by 92Composition.lengthNat.find_min · cited by 30Nat.find_minComposition.sizeUpTo · cited by 26Composition.sizeUpToComposition.index · cited by 9Composition.indexComposition.sizeUpTo_zero · cited by 3Composition.sizeUpTo_zeroComposition.index_exists · cited by 2Composition.index_existsComposition.sizeUpTo_index_leCITED BYCITES

Cites10

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.