mapL — Mathlib

English

Given a family of continuous linear maps f_i: E_i → E'_i, there is an induced continuous linear map mapL: ⨂ E_i → ⨂ E'_i implementing the componentwise application.

Русский

Для семейства непрерывных линейных отображений f_i: E_i → E'_i существует индуцированное отображение mapL: ⨂ E_i → ⨂ E'_i, реализующее применение по компонентам.

LaTeX

$$theorem mapL : (⨂ᵏ i, E i) →L[𝕜] ⨂ᵏ i, E' i$$

Lean4

/-- Let `Eᵢ` and `E'ᵢ` be two families of normed `𝕜`-vector spaces.
Let `f` be a family of continuous `𝕜`-linear maps between `Eᵢ` and `E'ᵢ`, i.e.
`f : Πᵢ Eᵢ →L[𝕜] E'ᵢ`, then there is an induced continuous linear map
`⨂ᵢ Eᵢ → ⨂ᵢ E'ᵢ` by `⨂ aᵢ ↦ ⨂ fᵢ aᵢ`.
-/
noncomputable def mapL : (⨂[𝕜] i, E i) →L[𝕜] ⨂[𝕜] i, E' i :=
  liftIsometry 𝕜 E _ <| (tprodL 𝕜).compContinuousLinearMap f

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