mul_const — Mathlib

English

Equivalences for counting measure: HasFiniteIntegral f μ ↔ tsum ∥f∥ < ∞ and related variants.

Русский

Эквивалентности для счетной меры: HasFiniteIntegral f μ ⇔ tsum ∥f∥ < ∞ и подобные варианты.

LaTeX

$$$HasFiniteIntegral f μ \iff tsum (\|f\|) < ∞$$$

Lean4

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

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