prod_prod — Mathlib

English

If s ⊆ α is measurable and t ⊆ β is measurable, then the product measure of the rectangles satisfies μ.prod ν (s × t) = μ(s) · ν(t).

Русский

Если s ⊆ α и t ⊆ β измеримы, то произведение мер по прямоугольникам равно μ(s) · ν(t).

LaTeX

$$$ (\mu \mathrm{prod} \nu)(s \times^{\mathrm{ˢ}} t) = \mu(s) \cdot \nu(t) $$$

Lean4

@[simp]
theorem prod_prod (s : Set α) (t : Set β) : μ.prod ν (s ×ˢ t) = μ s * ν t := by simp [coeFn_def]

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