integral_sub — Mathlib

English

If f and g are circle-integrable on the same circle, then the circle integral of f − g equals the difference of the circle integrals of f and g.

Русский

Если f и g кругово интегрируемы на одной окружности, то интеграл f−g равен разности интегралов от f и g.

LaTeX

$$$CircleIntegrable f c R \\to CircleIntegrable g c R \\Rightarrow \\oint z in C(c,R), (f(z) - g(z)) \\,dz = \\oint z in C(c,R), f(z) \\,dz - \\oint z in C(c,R), g(z) \\,dz$$$

Lean4

theorem integral_sub {f g : ℂ → E} {c : ℂ} {R : ℝ} (hf : CircleIntegrable f c R) (hg : CircleIntegrable g c R) :
    (∮ z in C(c, R), f z - g z) = (∮ z in C(c, R), f z) - ∮ z in C(c, R), g z := by
  simp only [circleIntegral, smul_sub, intervalIntegral.integral_sub hf.out hg.out]

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