English
The membership criterion mem_compPartialSumTarget_iff states that an i belongs to compPartialSumTarget m M N iff its length lies between m and M and all coordinates satisfy 1 ≤ blocks and blocksFun < N.
Русский
Критерий принадлежности в целевом множестве: i принадлежит compPartialSumTarget m M N тогда, когда длина i лежит между m и M, и для каждого координата выполняются 1 ≤ blocksFun и blocksFun < N.
LaTeX
$$$i ∈ compPartialSumTarget(m,M,N) \\iff m ≤ i.2.length ∧ i.2.length < M ∧ ∀ j : Fin i.2.length, i.2.blocksFun j < N.$$$
Lean4
/-- Target set in the change of variables to compute the composition of partial sums of formal
power series, here given a a finset.
See also `comp_partialSum`. -/
def compPartialSumTarget (m M N : ℕ) : Finset (Σ n, Composition n) :=
Set.Finite.toFinset <|
((Finset.finite_toSet _).dependent_image _).subset <| compPartialSumTargetSet_image_compPartialSumSource m M N
