sub — Mathlib

English

If hf and hg are Integrable, then f − g is Integrable.

Русский

Если f и g интегрируемы, то их разность f − g интегрируема.

LaTeX

$$$\text{Integrable } I\ l\ f\ vol \quad\Rightarrow\quad \text{Integrable } I\ l\ g\ vol \Rightarrow \text{Integrable } I\ l\ (f - g)\ vol$$$

Lean4

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

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