lintegral_le_edist_mul — Mathlib

English

For a bounded continuous f: X → ℝ≥0, the lintegral of f is bounded above by edist(0, f) times μ(univ).

Русский

Для ограниченной непрерывной f: X → ℝ≥0 линегральный интеграл ограничен сверху edist(0, f) умножить на μ(всё пространство).

LaTeX

$$$$\\int^{ - } x, f(x) \\partial \\mu \\le edist(0, f) \\cdot \\mu(\\mathrm{Set.univ}).$$$$

Lean4

theorem lintegral_le_edist_mul (f : X →ᵇ ℝ≥0) (μ : Measure X) : (∫⁻ x, f x ∂μ) ≤ edist 0 f * (μ Set.univ) :=
  le_trans (lintegral_mono (fun x ↦ ENNReal.coe_le_coe.mpr (f.apply_le_nndist_zero x))) (by simp)

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