sigmaFinite_tprod — Mathlib

English

For [∀ i, SigmaFinite (μ i)], the evaluation of pi' μ on universal product equals the product of μ i on s_i.

Русский

При условии SigmaFinite меры μ i, значение pi' μ на произведение s_i равно произведению μ_i(s_i).

LaTeX

$$\forall s, \text{pi'}(μ)(\pi univ s) = ∏_i μ_i(s_i)$$

Lean4

instance sigmaFinite_tprod (l : List δ) (μ : ∀ i, Measure (X i)) [∀ i, SigmaFinite (μ i)] :
    SigmaFinite (Measure.tprod l μ) := by
  induction l with
  | nil => rw [tprod_nil]; infer_instance
  | cons i l ih => rw [tprod_cons]; exact @prod.instSigmaFinite _ _ _ _ _ _ _ ih

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