integral_sub — Mathlib

English

If hf and hg are Integrable, then the integral of f − g equals the integral of f minus the integral of g.

Русский

Пусть hf и hg интегрируемы. Тогда интеграл по f−g равен интегралу по f минус интеграл по g.

LaTeX

$$$\text{Integrable } I\ l\ f\ vol \rightarrow \text{Integrable } I\ l\ g\ vol \rightarrow \int I l\ (f - g)\ vol = \int I l\ f\ vol - \int I l\ g\ vol$$$

Lean4

theorem integral_sub (hf : Integrable I l f vol) (hg : Integrable I l g vol) :
    integral I l (f - g) vol = integral I l f vol - integral I l g vol :=
  (hf.hasIntegral.sub hg.hasIntegral).integral_eq

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