instSemilinearIsometryEquivClass — Mathlib

English

The coercion map from LinearIsometryEquiv to the function space is injective: different isometry equivalences give different functions.

Русский

Коэрционационная карта из LinearIsometryEquiv в пространство функций инъективна: разные эквивалентности изометрий задают разные функции.

LaTeX

$$$\\mathrm{coe}_{\\mathrm{LI}}: (E \\simeq_{\\mathrm{LI}} E') \\to (E \\to E')$ is injective$$

Lean4

instance instSemilinearIsometryEquivClass : SemilinearIsometryEquivClass (E ≃ₛₗᵢ[σ₁₂] E₂) σ₁₂ E E₂
    where
  map_add f := map_add f.toLinearEquiv
  map_smulₛₗ e := map_smulₛₗ e.toLinearEquiv
  norm_map e := e.norm_map'

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