sub — Mathlib

English

If f and g are locally integrable on s, then f − g is locally integrable on s.

Русский

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

LaTeX

$$$\\text{LocallyIntegrableOn}(f,s,μ) \\land \\text{LocallyIntegrableOn}(g,s,μ) \\Rightarrow \\text{LocallyIntegrableOn}(f-g,s,μ)$$$

Lean4

protected theorem sub {f g : X → E} (hf : LocallyIntegrableOn f s μ) (hg : LocallyIntegrableOn g s μ) :
    LocallyIntegrableOn (f - g) s μ := fun x hx ↦ (hf x hx).sub (hg x hx)

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