average_neg

Mathlib.MeasureTheory.Integral.Average

URI: https://scilib.ai/kg/mathlib#MeasureTheory.average_neg

English

Average respects negation: average of -f is the negative of the average of f.

Русский

Среднее сохраняет отрицание: average(−f) = −average(f).

LaTeX

$$$\\laverage_{μ}(-f) = -\\laverage_{μ}(f)$$$

Lean4

@[simp]
theorem average_neg (f : α → E) : ⨍ x, -f x ∂μ = -⨍ x, f x ∂μ :=
  integral_neg f

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

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

Разделы

Аффилиация

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