piPremeasure_pi — Mathlib

English

In the finite-index setting, piPremeasure on the full product with universal domain equals the product of the marginals over i.

Русский

В конечном индексе piPremeasure на всем произведении равен произведению по частям.

LaTeX

$$\operatorname{piPremeasure}(m)(\mathrm{pi}\;\mathrm{univ}\; s) = \prod_i m_i(s_i)$$

Lean4

theorem piPremeasure_pi {s : ∀ i, Set (α i)} (hs : (pi univ s).Nonempty) :
    piPremeasure m (pi univ s) = ∏ i, m i (s i) := by simp [hs, piPremeasure]

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