setLIntegral_const

Mathlib.MeasureTheory.Integral.Lebesgue.Basic

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

English

For any set s and constant c, the lintegral over s of c equals c times μ(s).

Русский

Для множества s и константы c линеграл по s равен c·μ(s).

LaTeX

$$$$ \int^- x in s, c \partial \mu = c \cdot \mu(s). $$$$

Lean4

theorem setLIntegral_const (s : Set α) (c : ℝ≥0∞) : ∫⁻ _ in s, c ∂μ = c * μ s := by
  rw [lintegral_const, Measure.restrict_apply_univ]

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

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

Разделы

Аффилиация

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