compPartialSumTargetSet — Mathlib

English

There exists j in compPartialSumSource such that compChangeOfVariables j hj = i for any i in compPartialSumTargetSet; i.e., the target set is covered by the image of the source under the change of variables.

Русский

Существует j в compPartialSumSource такое, что compChangeOfVariables j hj = i для любого i в compPartialSumTargetSet; то есть целевое множество покрыто образом через источник.

LaTeX

$$$\\exists j\\, \\exists hj\\; (compChangeOfVariables\\ m\\ M\\ N\\ j\\ hj) = i.$$$

Lean4

/-- Target set in the change of variables to compute the composition of partial sums of formal
power series, here given a a set. -/
def compPartialSumTargetSet (m M N : ℕ) : Set (Σ n, Composition n) :=
  {i | m ≤ i.2.length ∧ i.2.length < M ∧ ∀ j : Fin i.2.length, i.2.blocksFun j < N}

Похожие утверждения