lintegral_sub_le' — Mathlib

English

A variant of lintegral_sub_le' for ENNReal with h f measurable, giving le inequalities between subtractions.

Русский

Вариант lintegral_sub_le' для ENNReal при измеримости f, дающий неравенства между вычитаниями.

LaTeX

$$$(f,g : α → ENNReal) (hf : AEMeasurable f μ) : ∫⁻ x, g(x) ∂μ - ∫⁻ x, f(x) ∂μ ≤ ∫⁻ x, g(x) ∂μ - ∫⁻ x, f(x) ∂μ$$$

Lean4

theorem lintegral_sub_le' (f g : α → ℝ≥0∞) (hf : AEMeasurable f μ) : ∫⁻ x, g x ∂μ - ∫⁻ x, f x ∂μ ≤ ∫⁻ x, g x - f x ∂μ :=
  by
  rw [tsub_le_iff_right]
  by_cases hfi : ∫⁻ x, f x ∂μ = ∞
  · rw [hfi, add_top]
    exact le_top
  · rw [← lintegral_add_right' _ hf]
    gcongr
    exact le_tsub_add

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