prod_restrict — Mathlib

English

Relates map prodAssoc to μ.prod ν via equality of measurable images.

Русский

Связь отображения prodAssoc с μ.prod ν через равенство образов по измеримым изображениям.

LaTeX

$$$\\operatorname{map}(\\text{prodAssoc})((μ.prod ν).prod τ) = μ.prod (ν.prod τ)$$$

Lean4

theorem prod_restrict (s : Set α) (t : Set β) : (μ.restrict s).prod (ν.restrict t) = (μ.prod ν).restrict (s ×ˢ t) :=
  by
  rw [← sum_sfiniteSeq μ, ← sum_sfiniteSeq ν, restrict_sum_of_countable, restrict_sum_of_countable, prod_sum, prod_sum,
    restrict_sum_of_countable]
  congr 1
  ext1 i
  refine prod_eq fun s' t' hs' ht' => ?_
  rw [restrict_apply (hs'.prod ht'), prod_inter_prod, prod_prod, restrict_apply hs', restrict_apply ht']

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