integral_smul — Mathlib

English

Equivalent restatement: the integral of the negation is the negation of the integral.

Русский

Эквивалентно: интеграл от отрицания есть − интеграла.

LaTeX

$$$\int a, (-f) a \partial\mu = -\int a, f a \partial\mu$$$

Lean4

theorem integral_smul {R : Type*} [NormedRing R] [Module R G] [IsBoundedSMul R G] [SMulCommClass ℝ R G] (c : R)
    {f : α → G} (hf : Integrable f μ) : ∫ a, c • f a ∂μ = c • ∫ a, f a ∂μ :=
  by
  by_cases hG : CompleteSpace G
  · simpa only [integral, hG, hf, hf.fun_smul c] using L1.integral_smul c (toL1 f hf)
  · simp [integral, hG]

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