instIsFiniteMeasureForallVolume — Mathlib

English

If every i-space α_i has finite volume, then the product volume measure on ∏ α_i is finite.

Русский

Если каждая объёмная мера(volume) на α_i конечна, то произведение объемов на произведении пространств ∏ α_i является конечной мерой.

LaTeX

$$$\operatorname{IsFiniteMeasure}(\mathrm{volume})$$$

Lean4

instance {α : ι → Type*} [∀ i, MeasureSpace (α i)] [∀ i, IsFiniteMeasure (volume : Measure (α i))] :
    IsFiniteMeasure (volume : Measure (∀ i, α i)) :=
  pi.instIsFiniteMeasure _

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