prod_right_ae — Mathlib

English

If f: α→R and g: β→E are integrable, then the product z ↦ f(z1) • g(z2) is integrable on α×β with respect to μ×ν.

Русский

Если f: α→R и g: β→E интегрируемы, то z↦f(z1)·g(z2) интегрируема на α×β по мере μ×ν.

LaTeX

$$$\mathrm{Integrable}(f, μ) \land \mathrm{Integrable}(g, ν) \Rightarrow \mathrm{Integrable}(z \mapsto f(z_1) \cdot g(z_2), μ×ν)$$$

Lean4

theorem prod_right_ae [SFinite μ] ⦃f : α × β → E⦄ (hf : Integrable f (μ.prod ν)) :
    ∀ᵐ x ∂μ, Integrable (fun y => f (x, y)) ν :=
  hf.swap.prod_left_ae

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