integrable_prod — Mathlib

English

A function f into a product space E × F is integrable iff its projections to E and F are integrable.

Русский

Функция f: α → E × F интегрируема тогда и только тогда, когда её проекции в E и F интегрируемы.

LaTeX

$$$ \\operatorname{Integrable}(f,\\mu) \\iff \\operatorname{Integrable}(x \\mapsto (f(x))_1,\\mu) \\land \\operatorname{Integrable}(x \\mapsto (f(x))_2,\\mu) $$$

Lean4

theorem integrable_prod {f : α → E × F} :
    Integrable f μ ↔ Integrable (fun x ↦ (f x).1) μ ∧ Integrable (fun x ↦ (f x).2) μ :=
  ⟨fun h ↦ ⟨h.fst, h.snd⟩, fun h ↦ h.1.prodMk h.2⟩

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