lintegral_mul_const' — Mathlib

English

For ENNReal r ≠ ∞ and Measurable f, ∫⁻ f a * r = (∫⁻ f a) * r.

Русский

Для r ≠ ∞ и измеримой f: ∫⁻ f a · r = (∫⁻ f a) · r.

LaTeX

$$$\forall r : \mathbb{R}_{\ge 0}^{\infty},\; {f : α \to \mathbb{R}_{\ge 0}^{\infty}}\; (hr : r \neq \infty) \Rightarrow ∫^- a, f a * r ∂μ = (∫^- a, f a ∂μ) * r$$$

Lean4

theorem lintegral_mul_const' (r : ℝ≥0∞) (f : α → ℝ≥0∞) (hr : r ≠ ∞) : ∫⁻ a, f a * r ∂μ = (∫⁻ a, f a ∂μ) * r := by
  simp_rw [mul_comm, lintegral_const_mul' r f hr]
    /- A double integral of a product where each factor contains only one variable
      is a product of integrals -/

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