mul_const — Mathlib

English

For a fixed scalar c, the map f ↦ c • f preserves integrability equivalence when c ≠ 0.

Русский

Для фиксированного скаляра c отображение f ↦ c • f сохраняет эквивалентность интегрируемости при c ≠ 0.

LaTeX

$$$\exists c \neq 0: \mathrm{Integrable}(f,\mu) \iff \mathrm{Integrable}(c \cdot f,\mu).$$$

Lean4

@[fun_prop]
theorem mul_const {f : α → 𝕜} (h : Integrable f μ) (c : 𝕜) : Integrable (fun x => f x * c) μ :=
  h.smul (MulOpposite.op c)

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