lintegral_mul_const_le — Mathlib

English

For ENNReal r and f, (∫ f) * r ≤ ∫ f * r.

Русский

Для ENNReal r и f: (∫ f) · r ≤ ∫ (f · r).

LaTeX

$$$\forall r : \mathbb{R}_{\ge 0}^{\infty},\; f : α \to \mathbb{R}_{\ge 0}^{\infty} \Rightarrow (\int^- a, f a ∂μ) \cdot r \le ∫^- a, f a \cdot r ∂μ$$$

Lean4

theorem lintegral_mul_const_le (r : ℝ≥0∞) (f : α → ℝ≥0∞) : (∫⁻ a, f a ∂μ) * r ≤ ∫⁻ a, f a * r ∂μ := by
  simp_rw [mul_comm, lintegral_const_mul_le r f]

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