fst — Mathlib

English

Define a kernel α → β from a kernel κ : α → β × γ by projecting onto the first component.

Русский

Определим ядро α → β из κ : α → β × γ путём проекции на первую компоненту.

LaTeX

$$$$\\text{fst }\\kappa := \\text{map }\\kappa \\mathrm{Prod.fst} \\;\\text{with measurability }\\; \\mathrm{measurable\\_fst}$$$$

Lean4

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

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