subtypeₗᵢ_toContinuousLinearMap

English

Let p be a submodule of a normed space E. The continuous linear map associated with the subtype inclusion equals the standard inclusion map viewed as a continuous linear map, i.e., the two constructions yield the same map.

Русский

Пусть p — подподпространство в нормированном пространстве E. Непрерывное линейное отображение, связанное с включением через подподмодулевую структуру, равно обычному включению, рассматриваемому как непрерывное линейное отображение.

LaTeX

$$$ p.subtype_{\\ell i}^{\\mathrm{toContinuousLinearMap}} = p.subtypeL $$$

Lean4

@[simp]
theorem subtypeₗᵢ_toContinuousLinearMap : p.subtypeₗᵢ.toContinuousLinearMap = p.subtypeL :=
  rfl

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