English
Let κ be a kernel from α × β to γ and b ∈ β with f : δ → α measurable. Then the comap of the left section (sectL κ b) along f equals the comap of κ along the map d ↦ (f d, b) with the appropriate product-measurability adjustment: comap (sectL κ b) f hf = comap κ (λ d, (f d, b)) (hf.prodMk measurable_const).
Русский
Пусть κ — ядро из α × β в γ и b ∈ β, а f : δ → α — измеримо. Тогда композиция обратной меры левого среза по f равна композиции обратной меры κ по отображению d ↦ (f d, b) с соответствующей мерой: comap (sectL κ b) f hf = comap κ (λ d, (f d, b)) (hf.prodMk measurable_const).
LaTeX
$$$\mathrm{comap}(\mathrm{sectL}\ κ\ b)\ f\ hf = \mathrm{comap}\ κ (\lambda d. (f d, b)) (hf.\,prodMk\, measurable\_const)$$$
Lean4
theorem comap_sectL (κ : Kernel (α × β) γ) (b : β) {f : δ → α} (hf : Measurable f) :
comap (sectL κ b) f hf = comap κ (fun d ↦ (f d, b)) (hf.prodMk measurable_const) :=
by
ext d s
rw [comap_apply, sectL_apply, comap_apply]
