sub — Mathlib

English

If f and g are integrable at l, then f − g is integrable at l: IntegrableAtFilter f l μ ∧ IntegrableAtFilter g l μ ⇒ IntegrableAtFilter (f − g) l μ.

Русский

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

LaTeX

$$$\\operatorname{IntegrableAtFilter}(f, l, \\mu) \\land \\operatorname{IntegrableAtFilter}(g, l, \\mu) \\Rightarrow \\operatorname{IntegrableAtFilter}(f - g, l, \\mu).$$$

Lean4

protected theorem sub {f g : α → E} (hf : IntegrableAtFilter f l μ) (hg : IntegrableAtFilter g l μ) :
    IntegrableAtFilter (f - g) l μ := by
  rw [sub_eq_add_neg]
  exact hf.add hg.neg

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