torusIntegral_neg — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem torusIntegral_neg (f : (ℂⁿ) → E) (c : ℂⁿ) (R : ℝⁿ) : (∯ x in T(c, R), -f x) = -∯ x in T(c, R), f x := by
  simp [torusIntegral, integral_neg]

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