compPartialSumTarget_tendsto_atTop

English

Theorem compChangeOfVariables_length states that the length of the composed object in the target equals the source length i.1.

Русский

Длина полученного после преобразования ChangeOfVariables равна длине источника: length( compChangeOfVariables ... ).snd = i.1.

LaTeX

$$$\\mathrm{Length}( (\\mathrm{compChangeOfVariables}\\ m\\ M\\ N\\ i\\ hi) ).snd = i.1$.$$

Lean4

/-- The auxiliary set corresponding to the composition of partial sums asymptotically contains
all possible compositions. -/
theorem compPartialSumTarget_tendsto_atTop : Tendsto (fun N => compPartialSumTarget 0 N N) atTop atTop := by
  apply Tendsto.comp compPartialSumTarget_tendsto_prod_atTop tendsto_atTop_diagonal

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