volume_eq_prod — Mathlib

English

The volume on the product space α × β is exactly the product of the volumes on α and β.

Русский

Объем на произведённом пространстве α × β равен произведению объёмов на α и β.

LaTeX

$$$ (\mathrm{volume} : \mathrm{Measure}(\alpha \times \beta)) = (\mathrm{volume} : \mathrm{Measure}\alpha).\mathrm{prod}(\mathrm{volume} : \mathrm{Measure}\beta) $$$

Lean4

theorem volume_eq_prod (α β) [MeasureSpace α] [MeasureSpace β] :
    (volume : Measure (α × β)) = (volume : Measure α).prod (volume : Measure β) :=
  rfl

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