setLIntegral_le_lintegral — Mathlib

English

The lintegral over a set is at most the lintegral over the entire space for the same function.

Русский

Линеграл по множеству не превосходит линеграла по всей области для той же функции.

LaTeX

$$$$ \int^- x in s, f(x) \partial μ \le \int^- x, f(x) \partial μ. $$$$

Lean4

theorem setLIntegral_le_lintegral (s : Set α) (f : α → ℝ≥0∞) : ∫⁻ x in s, f x ∂μ ≤ ∫⁻ x, f x ∂μ :=
  lintegral_mono' Measure.restrict_le_self le_rfl

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