English
There exists an affine map snd from P1 × P2 to P2 given by (p1, p2) ↦ p2, whose linear part is the second-coordinate projection on the vector components.
Русский
Существует аффинное отображение snd: P1 × P2 → P2, заданное изображением (p1, p2) ↦ p2, линейная часть которого — проекция на вторую координату в векторной части.
LaTeX
$$$\\exists \\mathrm{snd}: P_1 \\times P_2 \\to P_2 \\quad\\text{such that}\\quad \\mathrm{snd.toFun} = \\mathrm{Prod.snd} \\land \\mathrm{snd.linear} = \\mathrm{LinearMap.snd}_{k}(V_1,V_2).$$$
Lean4
/-- `Prod.snd` as an `AffineMap`. -/
def snd : P1 × P2 →ᵃ[k] P2 where
toFun := Prod.snd
linear := LinearMap.snd k V1 V2
map_vadd' _ _ := rfl
