English
The construction pi gives the finite product of outer measures across coordinates, i.e., a way to form a product outer measure on the product space from coordinate outer measures.
Русский
Построение pi даёт конечное произведение внешних мер по координатам, т.е. способ образования произведения внешних мер на произведении пространств.
LaTeX
$$\text{OuterMeasure.pi}(m) :\; \text{OuterMeasure}((i:ι)→α_i)$$
Lean4
/-- `OuterMeasure.pi m` is the finite product of the outer measures `{m i | i : ι}`.
It is defined to be the maximal outer measure `n` with the property that
`n (pi univ s) ≤ ∏ i, m i (s i)`, where `pi univ s` is the product of the sets
`{s i | i : ι}`. -/
protected def pi (m : ∀ i, OuterMeasure (α i)) : OuterMeasure (∀ i, α i) :=
boundedBy (piPremeasure m)
