dualEquivDual — Mathlib

English

There is a natural isomorphism between the dual of W and the range of W.dualLift.

Русский

Существует естественное изоморфизм между двойственным пространством W и образом W.dualLift.

LaTeX

$$dualEquivDual (W) : Module.Dual K W ≃ₗ[K] LinearMap.range W.dualLift$$

Lean4

/-- The natural isomorphism from the dual of a subspace `W` to `W.dualLift.range`. -/
noncomputable def dualEquivDual (W : Subspace K V) : Module.Dual K W ≃ₗ[K] LinearMap.range W.dualLift :=
  LinearEquiv.ofInjective _ dualLift_injective

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