Theorems · Definition · combinatorics

Composition.invEmbedding

{n : ℕ} → (c : Composition n) → (j : Fin n) → Fin (c.blocksFun (c.index j))

Mapping an element j of Fin n to the element in the block containing it, identified with Fin (c.blocksFun (c.index j)) through the canonical increasing bijection.

Defined in

Mathlib.Combinatorics.Enumerative.Composition

Cited by

5 results in Mathlib

Foundations

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