torusIntegral_sub — Mathlib

English

The torus integral is linear with respect to subtraction: torusIntegral(f - g) = torusIntegral(f) - torusIntegral(g).

Русский

Торо-интеграл линейен по отношению к вычитанию: torusIntegral(f - g) = torusIntegral(f) - torusIntegral(g).

LaTeX

$$$\operatorname{torusIntegral}(f-c,R) = \operatorname{torusIntegral}(f,R) - \operatorname{torusIntegral}(g,R)$$$

Lean4

theorem torusIntegral_sub (hf : TorusIntegrable f c R) (hg : TorusIntegrable g c R) :
    (∯ x in T(c, R), f x - g x) = (∯ x in T(c, R), f x) - ∯ x in T(c, R), g x := by
  simpa only [sub_eq_add_neg, ← torusIntegral_neg] using torusIntegral_add hf hg.neg

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