English
For a submodule p ⊆ E, the continuous linear map arising from the subtype inclusion coincides with the standard subtype inclusion as a continuous linear map.
Русский
Для подмодуля p ⊆ E непрерывное линейное отображение, порождаемое включением через подподмодульную структуру, совпадает с обычным включением как непрерывным линейным отображением.
LaTeX
$$$ p.subtype_{\\ell i}^{\\mathrm{toContinuousLinearMap}} = p.subtypeL $$$
Lean4
/-- `LinearIsometryEquivClass F R E E₂` asserts `F` is a type of bundled `R`-linear isometries
`M → M₂`.
This is an abbreviation for `SemilinearIsometryEquivClass F (RingHom.id R) E E₂`.
-/
abbrev LinearIsometryEquivClass (𝓕 : Type*) (R E E₂ : outParam Type*) [Semiring R] [SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂] [Module R E] [Module R E₂] [EquivLike 𝓕 E E₂] :=
SemilinearIsometryEquivClass 𝓕 (RingHom.id R) E E₂
