English
The blocks function of the auxiliary sigma composition at i equals the blocks function of a at embedding i in b.
Русский
Функция блоков вспомогательной сигма-композиции на i равна функции блоков a на встраивании i в b.
LaTeX
$$$blocksFun (\\mathrm{sigmaCompositionAux} a b \\langle i, (length_gather a b)^{-1} \\rangle) \\langle j, \\cdots \\rangle = blocksFun a (\\mathrm{embedding}\\ b\\ i\\ j)$$$
Lean4
/-- An auxiliary function used in the definition of `sigmaEquivSigmaPi` below, associating to
two compositions `a` of `n` and `b` of `a.length`, and an index `i` bounded by the length of
`a.gather b`, the subcomposition of `a` made of those blocks belonging to the `i`-th block of
`a.gather b`. -/
def sigmaCompositionAux (a : Composition n) (b : Composition a.length) (i : Fin (a.gather b).length) :
Composition ((a.gather b).blocksFun i)
where
blocks := (a.blocks.splitWrtComposition b)[i.val]'(by rw [length_splitWrtComposition, ← length_gather]; exact i.2)
blocks_pos {i}
hi :=
a.blocks_pos
(by
rw [← a.blocks.flatten_splitWrtComposition b]
exact mem_flatten_of_mem (List.getElem_mem _) hi)
blocks_sum := by simp [Composition.blocksFun, getElem_map, Composition.gather]
