prodLp_fst — Mathlib

English

If f ∈ L^1 with values in PiLp q E, then the integral of f has its first coordinate equal to the integral of the first coordinate function.

Русский

Если f ∈ L^1 со значениями в PiLp q E, то первая координата интеграла совпадает с интегралом первой координаты функции.

LaTeX

$$$$\\text{Integrable}(f,\\mu) \\Rightarrow \\Bigl(\\int x\\, f(x)\\,d\\mu\\Bigr)_{\\mathrm{fst}} = \\int x\\, (f(x))_{\\mathrm{fst}}\\,d\\mu.$$$$

Lean4

theorem prodLp_fst (h : Integrable f μ) : Integrable (fun x ↦ (f x).fst) μ :=
  integrable_prodLp_iff.1 h |>.1

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