neg — Mathlib

English

If f is interval integrable, then the function x ↦ -f(x) is interval integrable on the same interval.

Русский

Если f интервально интегрируема, то функция x ↦ -f(x) интервально интегрируема на том же интервале.

LaTeX

$$$$\text{IntervalIntegrable}(f, μ, a, b) \Rightarrow \text{IntervalIntegrable}(-f, μ, a, b).$$$$

Lean4

theorem neg {f : ℝ → E} (h : IntervalIntegrable f μ a b) : IntervalIntegrable (-f) μ a b :=
  ⟨h.1.neg, h.2.neg⟩

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