toMeasure_prod — Mathlib

English

Let μ and ν be finite measures on spaces α and β. Then the measure on α × β obtained by forming the product measure corresponds to the product of the individual toMeasure measures: toMeasure(μ × ν) = toMeasure(μ) × toMeasure(ν).

Русский

Пусть μ и ν — конечные меры на пространствах α и β. Тогда мера на пространстве α × β, получаемая как произведение этих мер, равна произведению соответствующих мер toMeasure: toMeasure(μ × ν) = toMeasure(μ) × toMeasure(ν).

LaTeX

$$$\operatorname{toMeasure}(\mu \mathrm{prod} \nu) = \operatorname{toMeasure}(\mu) \mathrm{prod} \operatorname{toMeasure}(\nu)$$$

Lean4

@[simp]
theorem toMeasure_prod : (μ.prod ν).toMeasure = μ.toMeasure.prod ν.toMeasure :=
  rfl

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