lintegral_mono_nnreal — Mathlib

English

The same as above; a variant with equality to ∫ f.

Русский

То же самое; вариант с равенством ∫ f.

LaTeX

$$$\forall f : α \to \mathbb{R}_{\ge 0}^{\infty},\; \text{Eq}\big( \big\lbrace ∫^- a, g a ∂μ : g \text{ measurable}, g ≤ f \big\rbrace, ∫^- a, f a ∂μ\big) = ∫^- a, f a ∂μ$$$

Lean4

theorem lintegral_mono_nnreal {f g : α → ℝ≥0} (h : f ≤ g) : ∫⁻ a, f a ∂μ ≤ ∫⁻ a, g a ∂μ :=
  lintegral_mono fun a => ENNReal.coe_le_coe.2 (h a)

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