integral_smul_nnreal_measure

Mathlib.MeasureTheory.Integral.Bochner.Basic

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

English

If c is a nonnegative real number (NNReal), then ∫ f d(c·μ) = c · ∫ f dμ.

Русский

Если c неотрицательное число, то ∫ f d(c·μ) = c · ∫ f dμ.

LaTeX

$$$$\int x, f x \partial( c \cdot \mu) = c \cdot \int x, f x \partial\mu.$$$

Lean4

@[simp]
theorem integral_smul_nnreal_measure (f : α → G) (c : ℝ≥0) : ∫ x, f x ∂(c • μ) = c • ∫ x, f x ∂μ :=
  integral_smul_measure f (c : ℝ≥0∞)

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

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

Разделы

Аффилиация

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