integral_pair — Mathlib

English

If f: X → E and g: X → F are integrable, then ∫ X (f(x), g(x)) dμ = (∫ f dμ, ∫ g dμ).

Русский

Если f: X → E и g: X → F интегрируемы, то интеграл пары равен паре интегралов: ∫ (f,g) = (∫ f, ∫ g).

LaTeX

$$$\\int_X (f(x),g(x)) \\,d\\mu = \\left(\\int_X f(x) \\,d\\mu, \\int_X g(x) \\,d\\mu\\right)$$$

Lean4

theorem integral_pair [CompleteSpace E] [CompleteSpace F] {f : X → E} {g : X → F} (hf : Integrable f μ)
    (hg : Integrable g μ) : ∫ x, (f x, g x) ∂μ = (∫ x, f x ∂μ, ∫ x, g x ∂μ) :=
  have := hf.prodMk hg
  Prod.ext (fst_integral this) (snd_integral this)

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