integrable_prodLp_iff — Mathlib

English

A function f: X → WithLp q (Prod E F) is integrable iff its first and second projections are integrable.

Русский

Функция f: X → WithLp q (Prod E F) интегрируема тогда и только тогда, когда интегрируемы ее проекции fst и snd.

LaTeX

$$$$\\text{Integrable}(f,\\mu) \\iff \\text{Integrable}(\\lambda x. (f x).fst, \\mu) \\land \\text{Integrable}(\\lambda x. (f x).snd, \\mu).$$$$

Lean4

theorem integrable_prodLp_iff : Integrable f μ ↔ Integrable (fun x ↦ (f x).fst) μ ∧ Integrable (fun x ↦ (f x).snd) μ :=
  by simp_rw [← memLp_one_iff_integrable, memLp_prodLp_iff]

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