lintegral_mono_set — Mathlib

English

Let f be a nonnegative measurable function on α and let s, t be subsets with s ⊆ t. Then the restricted lintegral over s is no larger than the lintegral over t.

Русский

Пусть f: α → ℝ≥0∞ и множества s ⊆ t. Тогда линегральный интеграл по s не превосходит линегральный интеграл по t: ∫_s f ≤ ∫_t f.

LaTeX

$$$$ \text{If } s \subseteq t, \quad \int^- x \in s, f(x) \partial \mu \le \int^- x \in t, f(x) \partial \mu.$$$$

Lean4

theorem lintegral_mono_set {_ : MeasurableSpace α} ⦃μ : Measure α⦄ {s t : Set α} {f : α → ℝ≥0∞} (hst : s ⊆ t) :
    ∫⁻ x in s, f x ∂μ ≤ ∫⁻ x in t, f x ∂μ :=
  lintegral_mono' (Measure.restrict_mono hst (le_refl μ)) (le_refl f)

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