integral_smul_measure

Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

URI: https://scilib.ai/kg/mathlib#intervalIntegral.integral_smul_measure

← MathLib Explorer

English

The integral of −c over [a,b] equals −(b−a)·c.

Русский

Интеграл по [a,b] константы −c равен −(b−a)·c.

LaTeX

$$$\int_{a}^{b} (-c) \, dμ = -(b - a) \cdot c$$$

Lean4

nonrec theorem integral_smul_measure (c : ℝ≥0∞) : ∫ x in a..b, f x ∂c • μ = c.toReal • ∫ x in a..b, f x ∂μ := by
  simp only [intervalIntegral, Measure.restrict_smul, integral_smul_measure, smul_sub]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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