mapEvalEquiv_apply

Mathlib.LinearAlgebra.Dual.Defs

URI: https://scilib.ai/kg/mathlib#Module.mapEvalEquiv_apply

English

For any submodule W of M, mapEvalEquiv R M W equals the image of W under Dual.eval: mapEvalEquiv(R,M) W = W.map(Dual.eval R M).

Русский

Для любого подпространства W ⊆ M выполняется mapEvalEquiv(R,M) W = W.map(Dual.eval R M).

LaTeX

$$mapEvalEquiv(R,M) W = W.map(Dual.eval(R,M)).$$

Lean4

@[simp]
theorem mapEvalEquiv_apply (W : Submodule R M) : mapEvalEquiv R M W = W.map (Dual.eval R M) :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru