fst_integral — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem fst_integral [CompleteSpace F] {f : X → E × F} (hf : Integrable f μ) : (∫ x, f x ∂μ).1 = ∫ x, (f x).1 ∂μ :=
  by
  by_cases hE : CompleteSpace E
  · exact ((ContinuousLinearMap.fst ℝ E F).integral_comp_comm hf).symm
  · have : ¬(CompleteSpace (E × F)) := fun h ↦ hE <| .fst_of_prod (β := F)
    simp [integral, *]

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