restrict_prod_eq_prod_univ — Mathlib

English

Restricting μ to s and ν to univ yields the same as restricting the product to s × univ.

Русский

Ограничение меры μ на s и ν на единичное множество эквивалентно ограничению произведения на s × univ.

LaTeX

$$$ (μ.restrict s).prod ν = (μ.prod ν).restrict (s ×ˢ univ) $$$

Lean4

theorem restrict_prod_eq_prod_univ (s : Set α) : (μ.restrict s).prod ν = (μ.prod ν).restrict (s ×ˢ univ) :=
  by
  have : ν = ν.restrict Set.univ := Measure.restrict_univ.symm
  rw [this, Measure.prod_restrict, ← this]

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