toContinuousLinearMap — Mathlib

English

Let f be a linear isometry between seminormed spaces E and E₂. Then f can be regarded as a continuous linear map from E to E₂ by pairing its linear part with its continuity datum.

Русский

Пусть f — линейная изометрия между полухарактеризующимися нормированными пространствами E и E₂. Тогда f можно рассматривать как непрерывное линейное отображение из E в E₂, сопоставив ему линейную часть и непрерывность.

LaTeX

$$$\mathrm{toContinuousLinearMap}(f) = \langle f_{toLinearMap}, f_{continuous} \rangle$$$

Lean4

/-- Interpret a linear isometry as a continuous linear map. -/
def toContinuousLinearMap : E →SL[σ₁₂] E₂ :=
  ⟨f.toLinearMap, f.continuous⟩

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