equivL — Mathlib

English

There is a continuous linear equivalence between C⋆ᵐᵒᵈ(A,E) and E, denoted by equivL.

Русский

Существует непрерывное линейное эквивалентство между C⋆ᵐᵒᵈ(A,E) и E, обозначаемое как equivL.

LaTeX

$$$ \text{equivL} : C⋆ᵐᵒᵈ(A,E) \simeq_L E $$$

Lean4

/-- `WithCStarModule.equiv` as a continuous linear equivalence between `C⋆ᵐᵒᵈ E` and `E`. -/
@[simps! apply symm_apply]
def equivL [Semiring R] [AddCommGroup E] [UniformSpace E] [Module R E] : C⋆ᵐᵒᵈ(A, E) ≃L[R] E :=
  { linearEquiv R A E with
    continuous_toFun := UniformEquiv.continuous uniformEquiv
    continuous_invFun := UniformEquiv.continuous uniformEquiv.symm }

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