setIntegral_univ

Mathlib.MeasureTheory.Integral.Bochner.Set

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

English

The integral over a set plus its complement equals the full integral.

Русский

Интеграл по множеству плюс его дополнение равен полному интегралу.

LaTeX

$$$\\int_{x \\in s} f(x) \\,d\\mu + \\int_{x \\in s^c} f(x) \\,d\\mu = \\int_{x} f(x) \\,d\\mu$$$

Lean4

theorem setIntegral_univ : ∫ x in univ, f x ∂μ = ∫ x, f x ∂μ := by rw [Measure.restrict_univ]

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

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

Разделы

Аффилиация

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