toContinuousSemilinearMapClass — Mathlib

English

Any semilinear isometry induces a structure of continuous semilinear maps.

Русский

Любое семилинейное изометрическое отображение порождает структуру непрерывных семилинейных отображений.

LaTeX

$$$\text{instance of ContinuousSemilinearMapClass}(\mathcal{F},\sigma_{12},E,E_2)$$$

Lean4

instance (priority := 100) toContinuousSemilinearMapClass [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] :
    ContinuousSemilinearMapClass 𝓕 σ₁₂ E E₂ where map_continuous := SemilinearIsometryClass.continuous

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