integrable_pair — Mathlib

English

If f and g are integrable, then the pair (f,g) is integrable.

Русский

Если f и g интегрируемы, то пара (f,g) интегрируема.

LaTeX

$$$\\mathrm{Integrable}(f,\\mu) \\Rightarrow \\mathrm{Integrable}(g,\\mu) \\Rightarrow \\mathrm{Integrable}(\\text{pair}(f,g),\\mu)$$$

Lean4

theorem integrable_pair {f : α →ₛ E} {g : α →ₛ F} : Integrable f μ → Integrable g μ → Integrable (pair f g) μ := by
  simpa only [integrable_iff_finMeasSupp] using FinMeasSupp.pair

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