lintegral_mono_set' — Mathlib

English

If s is contained in t up to μ-almost everywhere, then the lintegral of f over s is at most the lintegral over t.

Русский

Если s ⊆ t почти наверняка относительно μ, то ∫_s f ≤ ∫_t f.

LaTeX

$$$$ s \leq^{\mathrm{a.e.}}_{\mu} t \quad \Longrightarrow \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)

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