English
For a family of measures m_i on α_i, and a family of sets s_i in α_i, piPremeasure m (pi univ s) equals the product over i of m_i(s_i), provided the index set is finite.
Русский
Для конечного количества индексов верна формула: piPremeasure m (pi univ s) = ∏ i m_i(s_i).
LaTeX
$$\operatorname{piPremeasure}(m)(\pi\;\mathrm{univ}\;\,s) = \prod_{i} m_i(s_i)$$
Lean4
/-- An upper bound for the measure in a finite product space.
It is defined to by taking the image of the set under all projections, and taking the product
of the measures of these images.
For measurable boxes it is equal to the correct measure. -/
@[simp]
def piPremeasure (m : ∀ i, OuterMeasure (α i)) (s : Set (∀ i, α i)) : ℝ≥0∞ :=
∏ i, m i (eval i '' s)
