integral_neg

Mathlib.MeasureTheory.Integral.Bochner.L1

URI: https://scilib.ai/kg/mathlib#MeasureTheory.SimpleFunc.integral_neg

English

The integral of the negation of f equals the negation of the integral of f.

Русский

Интеграл от отрицания f равен − интегралу от f.

LaTeX

$$$$ \\int -f \\, dμ = -\\int f \\, dμ $$$$

Lean4

theorem integral_neg {f : α →ₛ E} (hf : Integrable f μ) : integral μ (-f) = -integral μ f :=
  setToSimpleFunc_neg _ weightedSMul_union hf

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru