zero_prod — Mathlib

English

The product of the zero measure with any finite measure is the zero measure: (0 : FiniteMeasure α).prod ν = 0.

Русский

Произведение нулевой меры с любой конечной мерой равно нулевой мере: (0 : FiniteMeasure α).prod ν = 0.

LaTeX

$$$\big(0 : \text{FiniteMeasure } \alpha\big) \mathrm{prod} \nu = 0$$$

Lean4

@[simp]
theorem zero_prod : (0 : FiniteMeasure α).prod ν = 0 := by rw [← mass_zero_iff, mass_prod, zero_mass, zero_mul]

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