fst — Mathlib

English

Let M1 and M2 be topological modules over a semiring R. The map that sends (x, y) in M1 × M2 to x in M1 is a continuous linear map from M1 × M2 to M1.

Русский

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

LaTeX

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

Lean4

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

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