pi'_pi — Mathlib

English

Re-statement: the pi' construction respects the product over coordinates and equals the product across i.

Русский

Повтор: конструктор pi' сохраняет произведение по координатам и равно произведению по i.

LaTeX

$$pi'_pi μ s = ∏_i μ_i(s_i)$$

Lean4

theorem pi'_pi [∀ i, SigmaFinite (μ i)] (s : ∀ i, Set (α i)) : pi' μ (pi univ s) = ∏ i, μ i (s i) := by
  classical
  rw [pi']
  rw [← MeasurableEquiv.piMeasurableEquivTProd_symm_apply, MeasurableEquiv.map_apply,
      MeasurableEquiv.piMeasurableEquivTProd_symm_apply, elim_preimage_pi, tprod_tprod _ μ, ← List.prod_toFinset,
      sortedUniv_toFinset] <;>
    exact sortedUniv_nodup ι

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