toSMul_apply

Mathlib.Analysis.BoxIntegral.Partition.Additive

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

English

The application of toSMul coincides with scalar multiplication on the box.

Русский

Применение toSMul совпадает с умножением на скаляр внутри коробки.

LaTeX

$$$f.toSMul(I) x = f(I) \cdot x$$$

Lean4

@[simp]
theorem toSMul_apply (f : ι →ᵇᵃ[I₀] ℝ) (I : Box ι) (x : E) : f.toSMul I x = f I • x :=
  rfl

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

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

Разделы

Аффилиация

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