setIntegral_mono

Mathlib.MeasureTheory.Integral.Bochner.Set

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

English

For a no-atom μ, the Bochner integral over [x, y] equals the integral over (x, y).

Русский

Для μ без атомов интеграл по [x, y] равен интегралу по (x, y).

LaTeX

$$$$\\int_{t \\in Icc\\,x\\,y} f(t)\\,d\\mu = \\int_{t \\in Ioo\\,x\\,y} f(t)\\,d\\mu.$$$$

Lean4

theorem setIntegral_mono (h : f ≤ g) : ∫ x in s, f x ∂μ ≤ ∫ x in s, g x ∂μ :=
  integral_mono hf hg h

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

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

Разделы

Аффилиация

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