integral_neg'

Mathlib.MeasureTheory.Integral.Bochner.Basic

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

English

If f and g are integrable, then the integral of f − g equals the integral of f minus the integral of g.

Русский

Если f и g интегрируемы, то интеграл от f − g равен интегралу f минус интеграл g.

LaTeX

$$$\int a, f(a) - g(a) \partial\mu = \int a, f(a) \partial\mu - \int a, g(a) \partial\mu$$$

Lean4

theorem integral_neg' (f : α → G) : ∫ a, (-f) a ∂μ = -∫ a, f a ∂μ :=
  integral_neg f

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

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

Разделы

Аффилиация

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