pi — Mathlib · SciLib

English

The finite product of measures is assembled via a product across coordinates.

Русский

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

LaTeX

$$FiniteMeasure.pi μ defined as product measure across i$$

Lean4

/-- The product of finitely many finite measures. -/
noncomputable def pi (μ : Π i, FiniteMeasure (α i)) : FiniteMeasure (Π i, α i) :=
  ⟨Measure.pi (fun i ↦ μ i), inferInstance⟩

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