integral_integral_add' — Mathlib

English

For f,g:β×γ→E, the integral of f+g equals the sum of the integrals over the two parts, reflecting linearity of the integral with respect to addition.

Русский

Интеграл от f+g равен сумме интегралов от f и g.

LaTeX

$$$\int f + \int g = \int (f+g)$$$

Lean4

theorem integral_integral_add' ⦃f g : β × γ → E⦄ (hf : Integrable f ((κ ⊗ₖ η) a)) (hg : Integrable g ((κ ⊗ₖ η) a)) :
    ∫ x, ∫ y, (f + g) (x, y) ∂η (a, x) ∂κ a = ∫ x, ∫ y, f (x, y) ∂η (a, x) ∂κ a + ∫ x, ∫ y, g (x, y) ∂η (a, x) ∂κ a :=
  Kernel.integral_integral_add hf hg

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