prod — Mathlib

English

Mass of the finite product equals the product of masses: mass(π μ) = ∏ μ_i.mass.

Русский

Масса произведения мер равна произведению масс отдельных мер.

LaTeX

$$$ (FiniteMeasure.pi μ).mass = \\prod i, (μ i).mass $$$

Lean4

/-- The binary product of finite measures. -/
noncomputable def prod (μ : FiniteMeasure α) (ν : FiniteMeasure β) : FiniteMeasure (α × β) :=
  ⟨μ.toMeasure.prod ν.toMeasure, inferInstance⟩

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