measureSpace — Mathlib

English

If α and β are measure spaces, then the product space α × β carries the product measure formed from the volume measures on α and β.

Русский

Если α и β – пространства с мерами, то произведение пространства α × β оснащено произведённой мерой, получаемой как произведение объёмных мер на α и β.

LaTeX

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

Lean4

instance measureSpace {α β} [MeasureSpace α] [MeasureSpace β] : MeasureSpace (α × β) where volume := volume.prod volume

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