neg — Mathlib

English

Negating f preserves integrability at a filter: IntegrableAtFilter f l μ ⇒ IntegrableAtFilter (−f) l μ.

Русский

При отрицании функции сохраняется интегрируемость на фильтре: IntegrableAtFilter f l μ ⇒ IntegrableAtFilter (−f) l μ.

LaTeX

$$$\\operatorname{IntegrableAtFilter}(f, l, \\mu) \\implies \\operatorname{IntegrableAtFilter}(-f, l, \\mu).$$$

Lean4

protected theorem neg {f : α → E} (hf : IntegrableAtFilter f l μ) : IntegrableAtFilter (-f) l μ :=
  by
  rcases hf with ⟨s, sl, hs⟩
  exact ⟨s, sl, hs.neg⟩

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