sum_partition_boxes — Mathlib

English

For a box-additive map f and I0, the sum over a partition of I of f equals the sum over the components determined by the chosen i.

Русский

Для box-additive отображения f и I0 сумма по разбиению I по f равна сумме по компонентам, определяемым выбранным i.

LaTeX

$$$\sum_{J \in \pi.boxes} f(J) = f(I)$$$

Lean4

theorem sum_partition_boxes (f : ι →ᵇᵃ[I₀] M) (hI : ↑I ≤ I₀) {π : Prepartition I} (h : π.IsPartition) :
    ∑ J ∈ π.boxes, f J = f I :=
  f.sum_partition_boxes' I hI π h

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