length_gather — Mathlib

English

The length of the auxiliary sigma composition equals the blocks function value.

Русский

Длина вспомогательной сигма-композиции равна значению функции блоков.

LaTeX

$$$\\mathrm{length}(\\mathrm{Composition.sigmaCompositionAux}(a,b,i)) = \\mathrm{blocksFun}(b,i)$$$

Lean4

theorem length_gather (a : Composition n) (b : Composition a.length) : length (a.gather b) = b.length :=
  show (map List.sum (a.blocks.splitWrtComposition b)).length = b.blocks.length by
    rw [length_map, length_splitWrtComposition]

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