sectL — Mathlib

English

Define sectL κ b as the comap of κ along a→(a,b) for a fixed b, i.e., sectL κ b = comap κ (λ a, (a,b)) (measurable_id.prodMk measurable_const).

Русский

Определим sectL κ b как сопоставление κ по отображению a ↦ (a,b) для фиксированного b: sectL κ b = comap κ (λa, (a,b)).

LaTeX

$$$\\text{sectL}(κ,b) = \\mathrm{comap}(κ, (\\lambda a. (a,b)), (\\mathrm{measurable\_id}.\\mathrm{prodMk} \\text{measurable\_const}))$$$

Lean4

/-- Define a `Kernel α γ` from a `Kernel (α × β) γ` by taking the comap of `fun a ↦ (a, b)` for
a given `b : β`. -/
noncomputable def sectL (κ : Kernel (α × β) γ) (b : β) : Kernel α γ :=
  comap κ (fun a ↦ (a, b)) (measurable_id.prodMk measurable_const)

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