weightedSMul_zero_measure — Mathlib

English

If the measure μ is the zero measure, then the weightedSmul map is identically zero: weightedSMul μ s = 0.

Русский

Если мера μ равна нулевой мере, то взвешенная умножение по любому множеству равно нулю.

LaTeX

$$$$weightedSMul(0)\, s = 0.$$$$

Lean4

@[simp]
theorem weightedSMul_zero_measure {m : MeasurableSpace α} : weightedSMul (0 : Measure α) = (0 : Set α → F →L[ℝ] F) := by
  ext1; simp [weightedSMul]

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