dualRestrict — Mathlib

English

For a submodule W ⊆ M, the dualRestrict map sends a functional on M to its restriction to W.

Русский

Для подмодуля W ⊆ M отображение dualRestrict отправляет функционал на M к его ограничению на W.

LaTeX

$$dualRestrict (W) : Module.Dual(R,M) →_R Module.Dual(R,W).$$

Lean4

/-- The `dualRestrict` of a submodule `W` of `M` is the linear map from the
  dual of `M` to the dual of `W` such that the domain of each linear map is
  restricted to `W`. -/
def dualRestrict (W : Submodule R M) : Module.Dual R M →ₗ[R] Module.Dual R W :=
  LinearMap.domRestrict' W

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