Theorems · Definition · several complex variables

Composition.gather

{n : ℕ} → (a : Composition n) → Composition a.length → Composition n

When a is a composition of n and b is a composition of a.length, a.gather b is the composition of n obtained by gathering all the blocks of a corresponding to a block of b. For instance, if a = [6, 5, 3, 5, 2] and b = [2, 3], one should gather together the first two blocks of a and its last three blocks, giving a.gather b = [11, 10].

Defined in

Mathlib.Analysis.Analytic.Composition

Cited by

5 results in Mathlib

Foundations

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