Theorems · Definition · combinatorics

Composition.boundary

{n : ℕ} → (c : Composition n) → Fin (c.length + 1) ↪o Fin (n + 1)

The i-th boundary of a composition, i.e., the leftmost point of the i-th block. We include a virtual point at the right of the last block, to make for a nice equiv with CompositionAsSet n.

Defined in

Mathlib.Combinatorics.Enumerative.Composition

Cited by

5 results in Mathlib

Foundations

Depth 32 from the axioms · uses propext, Classical.choice, Quot.sound