LinearIsometryClass — Mathlib

English

Definition turning a linear map from the scalar field into a continuous linear map.

Русский

Определение перехода линейной карты из поля скаляров в непрерывное линейное отображение.

LaTeX

$${𝕜 ↦ 𝕜 → E} → {𝕜 →L 𝕜 E}$$

Lean4

/-- `LinearIsometryClass F R E E₂` asserts `F` is a type of bundled `R`-linear isometries
`M → M₂`.

This is an abbreviation for `SemilinearIsometryClass F (RingHom.id R) E E₂`.
-/
abbrev LinearIsometryClass (𝓕 : Type*) (R E E₂ : outParam Type*) [Semiring R] [SeminormedAddCommGroup E]
    [SeminormedAddCommGroup E₂] [Module R E] [Module R E₂] [FunLike 𝓕 E E₂] :=
  SemilinearIsometryClass 𝓕 (RingHom.id R) E E₂

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