mapEvalEquiv — Mathlib

English

The isomorphism induced by evaluation, mapEvalEquiv, yields an order isomorphism between submodules of M and submodules of the double dual.

Русский

Изоморфизм, индуцируемый оцениванием, mapEvalEquiv, задаёт упорядоченное изоморфизм между подпространствами M и подпространствами двойственного двойственного пространства.

LaTeX

$$mapEvalEquiv : Submodule(R,M) \\cong_o Submodule(R, Dual(R, Dual(R,M))).$$

Lean4

/-- The isomorphism `Module.evalEquiv` induces an order isomorphism on subspaces. -/
def mapEvalEquiv : Submodule R M ≃o Submodule R (Dual R (Dual R M)) :=
  Submodule.orderIsoMapComap (evalEquiv R M)

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