dualLift_of_subtype — Mathlib

English

The dual lift is defined as an extension of a functional on W to a functional on V by choosing a complement to W.

Русский

Дуальный подъём задаётся как продолжение функционала на W до V путём выбора дополнения к W.

LaTeX

$$$\text{dualLift}(W): W^* \to V^*$ is an extension of any $\phi \in W^*$.$$

Lean4

@[simp]
theorem dualLift_of_subtype {φ : Module.Dual K W} (w : W) : W.dualLift φ (w : V) = φ w :=
  congr_arg φ <| DFunLike.congr_fun (Classical.choose_spec <| W.subtype.exists_leftInverse_of_injective W.ker_subtype) w

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