coe_mk

Mathlib.Analysis.BoxIntegral.Partition.Additive

URI: https://scilib.ai/kg/mathlib#BoxIntegral.BoxAdditiveMap.coe_mk

English

For a box-additive map f, and any partition π of a box I, the sum of f over the subboxes in π equals f(I).

Русский

Для(box-additive) отображения f и разбиения π коробки I сумма f по подокнам π равна f(I).

LaTeX

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

Lean4

@[simp]
theorem coe_mk (f h) : ⇑(mk f h : ι →ᵇᵃ[I₀] M) = f :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru