neg — Mathlib

English

Alternative formulation: the finset-sum of integrables is integrable.

Русский

Альтернативная формулировка: сумма по конечному множеству интегрируемых функций интегрируема.

LaTeX

$$$\\forall s: Finset\\, ι, \\forall f: ι\\to α\\to ε', (\\forall i∈s, Integrable (f i) μ) \\Rightarrow Integrable (s.sum (λ i, f i)) μ$$$

Lean4

/-- If `f` is integrable, then so is `-f`.
See `Integrable.neg'` for the same statement, but formulated with `x ↦ - f x` instead of `-f`. -/
@[fun_prop]
theorem neg {f : α → β} (hf : Integrable f μ) : Integrable (-f) μ :=
  ⟨hf.aestronglyMeasurable.neg, by fun_prop⟩

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