integral_integral_add_comp — Mathlib

English

Let f, g: γ → E integrable with respect to (η ∘ₖ κ) a. Then integrating the sum equals the sum of the integrals: ∫x ∫y (f(y) + g(y)) dηx(y) dκa = ∫x ∫y f(y) dηx(y) dκa + ∫x ∫y g(y) dηx(y) dκa.

Русский

Пусть f, g : γ → E интегрируемы; тогда двойной интеграл суммы равен сумме двойных интегралов.

LaTeX

$$$$ \\int x \\int y \\,(f(y) + g(y))\\,d\\eta_x(y)\\,d\\kappa a \n= \\int x \\int y \\! f(y)\\,d\\eta_x(y)\\,d\\kappa a + \\int x \\int y \\! g(y)\\,d\\eta_x(y)\\,d\\kappa a $$$$

Lean4

theorem integral_integral_add_comp ⦃f g : γ → E⦄ (hf : Integrable f ((η ∘ₖ κ) a)) (hg : Integrable g ((η ∘ₖ κ) a)) :
    ∫ x, ∫ y, f y + g y ∂η x ∂κ a = ∫ x, ∫ y, f y ∂η x ∂κ a + ∫ x, ∫ y, g y ∂η x ∂κ a :=
  (integral_fn_integral_add_comp id hf hg).trans <| integral_add hf.integral_comp hg.integral_comp

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