weightedSMul_empty — Mathlib

English

For any μ, the weightedSMul over the empty set is the zero map: weightedSMul μ ∅ = 0.

Русский

Для любой меры μ взвешенная умножение по пустому множеству даёт нулевую однозначную карту.

LaTeX

$$$$weightedSMul(\mu, \emptyset) = 0.$$$$

Lean4

@[simp]
theorem weightedSMul_empty {m : MeasurableSpace α} (μ : Measure α) : weightedSMul μ ∅ = (0 : F →L[ℝ] F) := by ext1 x;
  rw [weightedSMul_apply]; simp

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