swap_integral — Mathlib

English

For a function f: X → E × F integrable, the integral over μ of f equals the pair of integrals of its components: ∫ f = (∫ fst f, ∫ snd f).

Русский

Для интегрируемой функции f: X → E × F интеграл по μ равен паре интегралов по компонентам: ∫ f = (∫ fst f, ∫ snd f).

LaTeX

$$$\\int_X f(x) \\,d\\mu = \\left(\\int_X (\\text{fst}\\,f)(x) \\,d\\mu, \\int_X (\\text{snd}\\,f)(x) \\,d\\mu\\right)$$$

Lean4

theorem swap_integral (f : X → E × F) : (∫ x, f x ∂μ).swap = ∫ x, (f x).swap ∂μ :=
  .symm <| (ContinuousLinearEquiv.prodComm ℝ E F).integral_comp_comm f

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