pi — Mathlib · SciLib

English

The product measure on a finite product is defined as the finite product of the coordinate measures.

Русский

Произведение меры на конечном произведении определяется как конечное произведение координатных мер.

LaTeX

$$pi μ := product of μ_i over i$$

Lean4

instance _root_.MeasureTheory.MeasureSpace.pi {α : ι → Type*} [∀ i, MeasureSpace (α i)] : MeasureSpace (∀ i, α i) :=
  ⟨Measure.pi fun _ => volume⟩

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