integral_add_const — Mathlib

English

Let f be a BoundedContinuousFunction and c a real constant. The integral of f + c equals the integral of f plus μ(α) times c.

Русский

Пусть f — ограниченная непрерывная функция и c — константа. Интеграл по α функции f + c равен интегралу f плюс μ(α)·c.

LaTeX

$$$$\\int x, (f(x) + c) ∂μ = \\int x, f(x) ∂μ + μ(\\mathrm{real}\\, Set.univ) \\cdot c.$$$$

Lean4

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

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