mass_prod — Mathlib

English

The mass (total measure) of the product measure equals the product of the masses: mass(μ.prod ν) = mass(μ) · mass(ν).

Русский

Общая масса произведения мер равна произведению масс: mass(μ.prod ν) = mass(μ) mass(ν).

LaTeX

$$$\operatorname{mass}(\mu \mathrm{prod} \nu) = \operatorname{mass}(\mu) \cdot \operatorname{mass}(\nu).$$$

Lean4

@[simp]
theorem mass_prod : (μ.prod ν).mass = μ.mass * ν.mass :=
  by
  simp only [coeFn_def, mass, univ_prod_univ.symm, toMeasure_prod]
  rw [← ENNReal.toNNReal_mul]
  exact congr_arg ENNReal.toNNReal (Measure.prod_prod univ univ)

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