torusIntegral_add — Mathlib

English

The torus integral is linear: torusIntegral(f,c,R) + torusIntegral(g,c,R) = torusIntegral(f+g,c,R).

Русский

Торо-интеграл линейен: сумма интегралов равна интегралу суммы.

LaTeX

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

Lean4

theorem torusIntegral_add (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 [torusIntegral, smul_add, Pi.add_apply] using integral_add hf.function_integrable hg.function_integrable

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