setIntegral_const

Mathlib.MeasureTheory.Integral.Bochner.Set

URI: https://scilib.ai/kg/mathlib#MeasureTheory.setIntegral_const

English

Integrating a constant c over a set s equals the measure of s times c.

Русский

Интеграл константы c по множеству s равен мере множества s, умноженной на c.

LaTeX

$$$$ \int_{x \in s} c \, d\mu = (\mu.s) \cdot c $$$$

Lean4

theorem setIntegral_const [CompleteSpace E] (c : E) : ∫ _ in s, c ∂μ = μ.real s • c := by
  rw [integral_const, measureReal_restrict_apply_univ]

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

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

Разделы

Аффилиация

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