snd_integral — Mathlib

English

If f: X → E × F is integrable, then the second coordinate of the Bochner integral equals the integral of the second coordinate: (∫ f dμ).2 = ∫ (snd f) dμ.

Русский

Если f: X → E × F интегрируема, то вторая координата интеграла равна интегралу по второй координате: (∫ f dμ).2 = ∫ snd f dμ.

LaTeX

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

Lean4

theorem snd_integral [CompleteSpace E] {f : X → E × F} (hf : Integrable f μ) : (∫ x, f x ∂μ).2 = ∫ x, (f x).2 ∂μ :=
  by
  rw [← Prod.fst_swap, swap_integral]
  exact fst_integral <| hf.snd.prodMk hf.fst

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