smul_measure — Mathlib

English

If HasFiniteIntegral f μ holds and c ≠ ∞, then HasFiniteIntegral f (c • μ) holds.

Русский

Если HasFiniteIntegral f μ выполняется и c ≠ ∞, тогда HasFiniteIntegral f (c • μ) выполняется.

LaTeX

$$$HasFiniteIntegral f μ \\rightarrow (\\,c \\neq \\infty\\, ) \\rightarrow HasFiniteIntegral f (c \\cdot μ)$$$

Lean4

theorem smul_measure {f : α → ε} (h : HasFiniteIntegral f μ) {c : ℝ≥0∞} (hc : c ≠ ∞) : HasFiniteIntegral f (c • μ) :=
  by
  simp only [HasFiniteIntegral, lintegral_smul_measure] at *
  exact mul_lt_top hc.lt_top h

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