splitMany — Mathlib

English

If f is a function from boxes to an additive monoid, the sum of f over the boxes of split I i x equals the sum of f on the lower and upper pieces (with empties contributing zero).

Русский

Если f — функция с коробок в аддитивный моноид, сумма f по коробкам разбиения split I i x равна сумме f на нижнем и верхнем кусках (пустые дают ноль).

LaTeX

$$$\\big(\\sum J \\in (split I i x).boxes, f(J)\\big) = (I.splitLower i x).elim' 0\\, f + (I.splitUpper i x).elim' 0\\, f$$

Lean4

/-- Split a box along many hyperplanes `{y | y i = x}`; each hyperplane is given by the pair
`(i x)`. -/
def splitMany (I : Box ι) (s : Finset (ι × ℝ)) : Prepartition I :=
  s.inf fun p => split I p.1 p.2

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