English
For κ : Kernel (α × β) γ and a ∈ α, with f : δ → β measurable, the comap of sectR κ a along f equals the comap of κ along the map d ↦ (a, f d) with product measurability: comap (sectR κ a) f hf = comap κ (λ d, (a, f d)) (measurable_const.prodMk hf).
Русский
Для κ: ядро (α × β) γ и a ∈ α, с измеримой функцией f: δ → β, маcсово-комап секR κ a равен комап κ по отображению d ↦ (a, f d), с продуктовой мерой: comap (sectR κ a) f hf = comap κ (λ d, (a, f d)) (measurable_const.prodMk hf).
LaTeX
$$comap (sectR κ a) f hf = comap κ (λ d, (a, f d)) (measurable_const.prodMk hf)$$
Lean4
theorem comap_sectR (κ : Kernel (α × β) γ) (a : α) {f : δ → β} (hf : Measurable f) :
comap (sectR κ a) f hf = comap κ (fun d ↦ (a, f d)) (measurable_const.prodMk hf) :=
by
ext d s
rw [comap_apply, sectR_apply, comap_apply]
