dualAnnihilator_dualAnnihilator_eq

English

In the finite-dimensional setting, W.dualAnnihilator.dualAnnihilator equals Module.mapEvalEquiv(K,V,W).

Русский

В конечномерном случае W^⊥⊥ совпадает с образом W через отображение оценки.

LaTeX

$$W.dualAnnihilator.dualAnnihilator = Module.mapEvalEquiv K V W$$

Lean4

theorem dualAnnihilator_dualAnnihilator_eq (W : Subspace K V) :
    W.dualAnnihilator.dualAnnihilator = Module.mapEvalEquiv K V W :=
  by
  have : _ = W := Subspace.dualAnnihilator_dualCoannihilator_eq
  rw [dualCoannihilator, ← Module.mapEvalEquiv_symm_apply] at this
  rwa [← OrderIso.symm_apply_eq]

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