lintegral_mono_measure — Mathlib

English

The lintegral is monotone in both the function and the measure: if f ≤ g and μ ≤ ν, then f.lintegral μ ≤ g.lintegral ν.

Русский

Линеграль монотонен по функции и по мере: если f ≤ g и μ ≤ ν, то f.lintegral μ ≤ g.lintegral ν.

LaTeX

$$$f \\le g \\;\\wedge\\; μ \\le ν \\Longrightarrow f.lintegral μ \\le g.lintegral ν$$$

Lean4

theorem lintegral_mono_measure {f : α →ₛ ℝ≥0∞} (h : μ ≤ ν) : f.lintegral μ ≤ f.lintegral ν :=
  by
  simp only [lintegral]
  gcongr
  apply h

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