monotone_lintegral

Mathlib.MeasureTheory.Integral.Lebesgue.Basic

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

English

If f ≤ g pointwise, then the lintegral with respect to μ preserves the order: ∫ f ≤ ∫ g.

Русский

Если f(x) ≤ g(x) для всех x, то ∫ f dμ ≤ ∫ g dμ.

LaTeX

$$$$ f \le g \quad \Rightarrow \quad \int^- x, f(x) \partial \mu \le \int^- x, g(x) \partial \mu. $$$$

Lean4

theorem monotone_lintegral {_ : MeasurableSpace α} (μ : Measure α) : Monotone (lintegral μ) :=
  lintegral_mono

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

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

Разделы

Аффилиация

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