integral_sub

Mathlib.MeasureTheory.Integral.Bochner.L1

URI: https://scilib.ai/kg/mathlib#MeasureTheory.L1.integral_sub

← MathLib Explorer

English

The integral respects subtraction: ∫ (f − g) = ∫ f − ∫ g.

Русский

Интеграл сохраняет вычитание: ∫ (f − g) = ∫ f − ∫ g.

LaTeX

$$$\int (f - g) \, d\mu = \int f \, d\mu - \int g \, d\mu$$$

Lean4

@[integral_simps]
theorem integral_sub (f g : α →₁[μ] E) : integral (f - g) = integral f - integral g :=
  by
  simp only [integral]
  exact map_sub integralCLM f g

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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