snd — Mathlib

English

From a kernel κ : α → β × γ, construct a kernel snd κ : α → γ by projecting onto the second coordinate; equivalently, snd κ is the pushforward of κ by the second projection.

Русский

Из ядра κ : α → β × γ строится ядро snd κ : α → γ через проекцию на вторую координату; snd κ есть образ по второй проекции.

LaTeX

$$$snd \\kappa = mapOfMeasurable \\kappa \\mathrm{Prod.snd} \\; (\\text{measurable\_snd})$$$

Lean4

/-- Define a `Kernel α γ` from a `Kernel α (β × γ)` by taking the map of the second projection.
We use `mapOfMeasurable` for better defeqs. -/
noncomputable def snd (κ : Kernel α (β × γ)) : Kernel α γ :=
  mapOfMeasurable κ Prod.snd measurable_snd

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