snd — Mathlib

English

Let M1 and M2 be topological R-modules. The map Q1: M1 × M2 → M2 that sends (x, y) to y is a continuous linear map.

Русский

Пусть M1 и M2 — топологические модули над R. Отображение Q1: M1 × M2 → M2, задающее (x,y) ↦ y, является непрерывным линейным отображением.

LaTeX

$$$P_2: M_1 \times M_2 \to M_2, \quad P_2(x,y)=y, \quad P_2 \in L_R(M_1\times M_2, M_2).$$$

Lean4

/-- `Prod.snd` as a `ContinuousLinearMap`. -/
def snd : M₁ × M₂ →L[R] M₂ where
  cont := continuous_snd
  toLinearMap := LinearMap.snd R M₁ M₂

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