English
Let f,g: α×β → E be integrable with respect to μ×ν. Then the double integral of (f−g) equals the double integral of f minus the double integral of 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 subtraction. -/
theorem integral_integral_sub ⦃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_sub id hf hg).trans <| integral_sub hf.integral_prod_left hg.integral_prod_left
