lintegral_mono' — Mathlib

English

If μ ≤ ν and f ≤ g pointwise, then ∫ f ≤ ∫ g for ENNReal integrals.

Русский

Если μ ≤ ν и f ≤ g по точкам, тогда ∫ f ≤ ∫ g для интегралов Лебега.

LaTeX

$$$\forall f,g : α \to \mathbb{R}_{\ge 0}^{\infty},\; (hμν : μ ≤ ν) (hfg : f ≤ g) \Rightarrow ∫^- a, f a \partial μ ≤ ∫^- a, g a \partial ν$$$

Lean4

@[mono]
theorem lintegral_mono' {m : MeasurableSpace α} ⦃μ ν : Measure α⦄ (hμν : μ ≤ ν) ⦃f g : α → ℝ≥0∞⦄ (hfg : f ≤ g) :
    ∫⁻ a, f a ∂μ ≤ ∫⁻ a, g a ∂ν := by
  rw [lintegral, lintegral]
  exact
    iSup_mono fun φ =>
      iSup_mono' fun hφ =>
        ⟨le_trans hφ hfg, lintegral_mono (le_refl φ) hμν⟩
          -- version where `hfg` is an explicit forall, so that `@[gcongr]` can recognize it

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