Theorems · Theorem · combinatorics
CompositionAsSet.card_boundaries_eq_succ_length
∀ {n : ℕ} (c : CompositionAsSet n), c.boundaries.card = c.length + 1- Cited by
- 4 results in Mathlib
- Foundations
- Depth 63 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finset.cardstatement · cited by 2,327
- CompositionAsSetstatement and proof · cited by 26
- CompositionAsSet.boundariesstatement · cited by 18
- tsub_eq_iff_eq_add_of_leproof · cited by 12
- CompositionAsSet.lengthstatement · cited by 11
- CompositionAsSet.card_boundaries_posproof · cited by 3
Cited by4
Results whose statement or proof uses this declaration.
- CompositionAsSet.blocks_partial_sumproof · cited by 3
- CompositionAsSet.length_lt_card_boundariesproof · cited by 2
- CompositionAsSet.toComposition_boundariesproof · cited by 0
- Composition.toCompositionAsSet_blocksproof · cited by 0