instIsFiniteMeasureProdVolume — Mathlib

English

If spaces are standard measure spaces, the product space has volume equal to the product of volumes on each space.

Русский

Если пространства являются стандартными мерами, объём произведения равен произведению объёмов каждого пространства.

LaTeX

$$$\mathrm{volume}_{\alpha \times \beta} = \mathrm{volume}_\alpha \cdot \mathrm{volume}_\beta$$$

Lean4

instance {α β : Type*} [MeasureSpace α] [MeasureSpace β] [IsFiniteMeasure (volume : Measure α)]
    [IsFiniteMeasure (volume : Measure β)] : IsFiniteMeasure (volume : Measure (α × β)) :=
  prod.instIsFiniteMeasure _ _

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