integral_prod_swap — Mathlib

English

For any f, the integral over ν×μ of f(z.swap) equals the integral over μ×ν of f(z).

Русский

Для любой f интеграл по ν×μ от f(z.swap) равен интегралу по μ×ν от f(z).

LaTeX

$$$\int f(z\!\text{.swap}) \, d(ν×μ) = \int f(z) \, d(μ×ν)$$$

Lean4

theorem integral_prod_swap (f : α × β → E) : ∫ z, f z.swap ∂ν.prod μ = ∫ z, f z ∂μ.prod ν :=
  measurePreserving_swap.integral_comp MeasurableEquiv.prodComm.measurableEmbedding _

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