integral_integral_add — Mathlib

English

Let f,g: α×β → E be integrable with respect to μ×ν. Then the double integral of f+g equals the sum of the double integrals of f and g.

Русский

Пусть f,g: α×β → E интегрируемы по μ×ν. Тогда двойной интеграл от (f+g) равен сумме двойных интегралов от f и от g.

LaTeX

$$$$\\int\\int (f(x,y) + g(x,y)) \\, dν \\, dμ = \\int\\int f(x,y) \\, dν \\, dμ + \\int\\int g(x,y) \\, dν \\, dμ.$$$$

Lean4

/-- Double integrals commute with addition. -/
theorem integral_integral_add ⦃f g : α × β → E⦄ (hf : Integrable f (μ.prod ν)) (hg : Integrable g (μ.prod ν)) :
    (∫ x, ∫ y, f (x, y) + g (x, y) ∂ν ∂μ) = (∫ x, ∫ y, f (x, y) ∂ν ∂μ) + ∫ x, ∫ y, g (x, y) ∂ν ∂μ :=
  (integral_fn_integral_add id hf hg).trans <| integral_add hf.integral_prod_left hg.integral_prod_left

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