integrable_pi_iff — Mathlib

English

For a finite index set, a function f: X → Π_i E_i is integrable iff each coordinate function f_i is integrable with respect to μ.

Русский

Для конечного множества индексов функция f: X → Π_i E_i интегрируема тогда и только тогда, когда каждая координата f_i интегрируема по мере μ.

LaTeX

$$$$\\text{Integrable}(f,\\mu) \\iff \\forall i, \\text{Integrable}(f\\cdot i,\\mu).$$$$

Lean4

theorem integrable_pi_iff : Integrable f μ ↔ ∀ i, Integrable (f · i) μ := by
  simp_rw [← memLp_one_iff_integrable, memLp_pi_iff]

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