instIsFiniteMeasureOnCompactsProdVolume

English

If volume is finite on α and β, then it is finite on the product space for compact sets.

Русский

Если объем конечен на α и β, то он конечен на произведении в отношении компактных множеств.

LaTeX

$$$\text{IsFiniteMeasureOnCompacts}(\mathrm{volume}_{\alpha}) \land \text{IsFiniteMeasureOnCompacts}(\mathrm{volume}_{\beta}) \Rightarrow \text{IsFiniteMeasureOnCompacts}(\mathrm{volume}_{\alpha \times \beta})$$$

Lean4

instance {X Y : Type*} [TopologicalSpace X] [MeasureSpace X] [IsFiniteMeasureOnCompacts (volume : Measure X)]
    [TopologicalSpace Y] [MeasureSpace Y] [IsFiniteMeasureOnCompacts (volume : Measure Y)] :
    IsFiniteMeasureOnCompacts (volume : Measure (X × Y)) :=
  prod.instIsFiniteMeasureOnCompacts _ _

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