prodSnd — Mathlib

English

There is a canonical projection from the product X × Y to Y, denoted prodSnd, formed similarly to prodFst.

Русский

Существует каноническое отображение из произведения X × Y в Y, обозначаемое как prodSnd.

LaTeX

$$$\\text{prodSnd} : X \\times Y \\to Y$$$

Lean4

/-- The second projection from the product. -/
abbrev prodSnd {X Y : TopCat.{u}} : TopCat.of (X × Y) ⟶ Y :=
  ofHom { toFun := Prod.snd }

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