English
If κ: α→β and η: α→δ are s-finite, and f: β→γ, g: δ→ε are measurable, then (κ.map f) ×K (η.map g) equals (κ ×K η).map (Prod.map f g).
Русский
Если κ:α→β и η:α→δ — s-финитные ядра, а f:β→γ, g:δ→ε измеримы, то произведение карт продукта с картами эквивалентно отображению на произведение: (κ.map f) ×K (η.map g) = (κ ×K η).map (Prod.map f g).
LaTeX
$$$\\displaystyle (\\kappa.map f) \\times_K (\\eta.map g) = (\\kappa \\times_K \\eta).map (Prod.map f g)$$$
Lean4
theorem map_prod_map {ε} {mε : MeasurableSpace ε} (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel α δ)
[IsSFiniteKernel η] {f : β → γ} (hf : Measurable f) {g : δ → ε} (hg : Measurable g) :
(κ.map f) ×ₖ (η.map g) = (κ ×ₖ η).map (Prod.map f g) :=
by
ext1 x
rw [map_apply _ (hf.prodMap hg), prod_apply κ, ← Measure.map_prod_map _ _ hf hg, prod_apply, map_apply _ hf,
map_apply _ hg]
