integral_const_sub — Mathlib

English

For f: X → Real bounded, integral of f + c equals integral of f plus μ(univ) times c, etc.

Русский

Для ограниченного f: X → Real интеграл f + c равен интегралу f плюс μ(univ)·c.

LaTeX

$$$$\\int x, (f(x) + c) ∂μ = \\int x, f(x) ∂μ + μ.real Set.univ · c.$$$$

Lean4

theorem integral_const_sub (f : X →ᵇ ℝ) (c : ℝ) : ∫ x, (const X c - f) x ∂μ = μ.real Set.univ • c - ∫ x, f x ∂μ := by
  simp [integral_sub (integrable_const c) (f.integrable _)]

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