English
For any subspace W ⊆ V and φ ∈ W*, there exists an extension Φ ∈ V* that extends φ from W to V.
Русский
Для подпространства W ⊆ V и φ ∈ W*, существует продолжение Φ ∈ V*, которое расширяет φ от W к V.
LaTeX
$$$\exists \Phi \in V^*:\ \Phi|_{W} = \phi$$$
Lean4
/-- Given a subspace `W` of `V` and an element of its dual `φ`, `dualLift W φ` is
an arbitrary extension of `φ` to an element of the dual of `V`.
That is, `dualLift W φ` sends `w ∈ W` to `φ x` and `x` in a chosen complement of `W` to `0`. -/
noncomputable def dualLift (W : Subspace K V) : Module.Dual K W →ₗ[K] Module.Dual K V :=
(Classical.choose <| W.subtype.exists_leftInverse_of_injective W.ker_subtype).dualMap
