integral_mul_const — Mathlib

English

A constant function factor can be moved outside the integral: ∫ f·c = (∫ f)·c.

Русский

Постоянный множитель можно вынести за интеграл: ∫ f·c = (∫ f)·c.

LaTeX

$$$\int a, f(a) \cdot r \partial\mu = (\int a, f(a) \partial\mu) \cdot r$$$

Lean4

theorem integral_mul_const {L : Type*} [RCLike L] (r : L) (f : α → L) : ∫ a, f a * r ∂μ = (∫ a, f a ∂μ) * r := by
  simp only [mul_comm, integral_const_mul r f]

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