integral_integral_add' — Mathlib

English

Let f,g: α×β → E be integrable with respect to μ×ν. Then the double integral of f−g equals the difference 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. This is the version with `(f + g) (x, y)`
  (instead of `f (x, y) + g (x, y)`) in the LHS. -/
theorem integral_integral_add' ⦃f g : α × β → E⦄ (hf : Integrable f (μ.prod ν)) (hg : Integrable g (μ.prod ν)) :
    (∫ x, ∫ y, (f + g) (x, y) ∂ν ∂μ) = (∫ x, ∫ y, f (x, y) ∂ν ∂μ) + ∫ x, ∫ y, g (x, y) ∂ν ∂μ :=
  integral_integral_add hf hg

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