setIntegral_empty

Mathlib.MeasureTheory.Integral.Bochner.Set

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

English

The integral over the whole space equals the integral with no restriction.

Русский

Интеграл по всему пространству равен интегралу без ограничений.

LaTeX

$$$\\int_{x \\in \\mathrm{univ}} f(x) \\,d\\mu = \\int_{x} f(x) \\,d\\mu$$$

Lean4

theorem setIntegral_empty : ∫ x in ∅, f x ∂μ = 0 := by rw [Measure.restrict_empty, integral_zero_measure]

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

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

Разделы

Аффилиация

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