zero_mconv — Mathlib

English

Convolution with the zero measure yields the zero measure: 0 ∗ μ = 0.

Русский

Свёртка нулевой меры с любой мерой даёт нулевую меру.

LaTeX

$$$ 0 ∗ μ = 0 $$$

Lean4

/-- Convolution of the zero measure with a measure μ returns the zero measure. -/
@[to_additive (attr := simp) /-- Convolution of the zero measure with a measure μ returns
    the zero measure. -/
    ]
theorem zero_mconv (μ : Measure M) : (0 : Measure M) ∗ₘ μ = (0 : Measure M) :=
  by
  unfold mconv
  simp

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