dualRestrict_comp_dualLift — Mathlib

English

The composition dualRestrict ∘ dualLift is the identity on W*, i.e., dualRestrict(W) (dualLift(W)(φ)) = φ.

Русский

Произведение dualRestrict ∘ dualLift есть тождественное отображение на W*, то есть dualRestrict_W( dualLift_W(φ) ) = φ.

LaTeX

$$$(dualRestrict_W) \circ (dualLift_W) = \mathrm{id}_{W^*}$$$

Lean4

@[simp]
theorem dualRestrict_comp_dualLift (W : Subspace K V) : W.dualRestrict.comp W.dualLift = 1 :=
  by
  ext φ x
  simp

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