weightedSMul_smul_measure — Mathlib

English

If c is ENNReal and s is a set, then weightedSMul with density c • μ satisfies (weightedSMul (c • μ) s) = c.toReal • weightedSMul μ s.

Русский

Если параметр плотности умножить на ENNReal, то взвешенная умножение плотности удовлетворяет равенству: weightedSMul (c · μ) s = c.toReal · weightedSMul μ s.

LaTeX

$$$$weightedSMul(c \cdot \mu)\, s = c^{\toReal} \cdot weightedSMul\,\mu\, s.$$$$

Lean4

theorem weightedSMul_smul_measure {m : MeasurableSpace α} (μ : Measure α) (c : ℝ≥0∞) {s : Set α} :
    (weightedSMul (c • μ) s : F →L[ℝ] F) = c.toReal • weightedSMul μ s :=
  by
  ext1 x
  simp [weightedSMul_apply, smul_smul]

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