map_dualCoannihilator — Mathlib

English

If W is a subspace of the dual space V*, then applying the evaluation map to its dual coannihilator yields its dual annihilator: dualCoannihilator(W) mapped by ev_V equals dualAnnihilator(W).

Русский

Пусть W — подпространство в V*. Применение отображения эвалюации к его двойной коаннигиляции восстанавливает двойной аннигилятор: ev_V(W^⟂) = W^⊥.

LaTeX

$$$$ \\mathrm{dualCoannihilator}(W) \\xrightarrow{\\;ev_V\\;} W^{\\perp} \\\\text{(in } V^{**}) = W^{\\perp}. $$$$

Lean4

theorem map_dualCoannihilator (W : Subspace K (Dual K V)) [FiniteDimensional K V] :
    W.dualCoannihilator.map (Dual.eval K V) = W.dualAnnihilator := by
  rw [← dualAnnihilator_dualAnnihilator_eq_map, dualCoannihilator_dualAnnihilator_eq]

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