sectR — Mathlib

English

For κ : Kernel (α × β) γ, and a ∈ α, b ∈ β, the right-section at a satisfies (sectR κ a) b = κ(a, b).

Русский

Для κ: ядро (α × β) γ и для любых a ∈ α, b ∈ β верно: (sectR κ a) b = κ(a, b).

LaTeX

$$sectR κ a b = κ(a, b)$$

Lean4

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

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