English
The mapping compPartialSumTargetSet collects all index pairs (n, c) that correspond to valid compositions appearing in the partial sums; in particular, it is the Finset of pairs (n, c) with n appropriate and c a valid composition.
Русский
Отбор частичных сумм через смену переменных: compPartialSumTargetSet собирает все пары индексов (n, c), соответствующие допустимой композиции в частичных суммах.
LaTeX
$$$\\text{compPartialSumTargetSet}(m,M,N) = \\{ (n, c) \\mid n, c \\text{ удовлетворяют условиям для композиции}\\}$.$$
Lean4
theorem compChangeOfVariables_blocksFun (m M N : ℕ) {i : Σ n, Fin n → ℕ} (hi : i ∈ compPartialSumSource m M N)
(j : Fin i.1) :
(compChangeOfVariables m M N i hi).2.blocksFun ⟨j, (compChangeOfVariables_length m M N hi).symm ▸ j.2⟩ = i.2 j :=
by
rcases i with ⟨n, f⟩
dsimp [Composition.blocksFun, Composition.blocks, compChangeOfVariables]
simp only [List.getElem_ofFn]
