snd — Mathlib

English

The projection to the second coordinate is the map snd, sending a pair to its second component.

Русский

Проекция на вторую координату — это отображение snd, отправляющее пару во вторую компоненту.

LaTeX

$$$\\mathrm{snd}(p,p')(x)=x.2$$$

Lean4

/-- Projection to the second coordinate as a `LinearPMap` -/
protected def snd (p : Submodule R E) (p' : Submodule R F) : E × F →ₗ.[R] F
    where
  domain := p.prod p'
  toFun := (LinearMap.snd R E F).comp (p.prod p').subtype

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