integral_add — Mathlib

English

For simple functions f,g in L1, the integral is additive: ∫ (f+g) dμ = ∫ f dμ + ∫ g dμ.

Русский

Для простых функций f,g в L1 интеграл аддитивен: ∫(f+g) dμ = ∫ f dμ + ∫ g dμ.

LaTeX

$$$\int (f + g) \, d\mu = \int f \, d\mu + \int g \, d\mu$$$

Lean4

theorem integral_add (f g : α →₁ₛ[μ] E) : integral (f + g) = integral f + integral g :=
  setToL1S_add _ (fun _ _ => weightedSMul_null) weightedSMul_union _ _

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