map_le_dualAnnihilator_dualAnnihilator

English

For a subspace W of V, the image of W under the canonical evaluation map from V to V** is contained in the double annihilator (W^⊥)^⊥.

Русский

Для подпространства W ⊆ V образ W под каноническим оценочным отображением V → V** содержится в (W^⊥)^⊥.

LaTeX

$$$\mathrm{ev}(W) \subseteq (W^{\perp})^{\perp}$, where $\mathrm{ev}: V \to V^{**}$ is the evaluation map.$$

Lean4

theorem map_le_dualAnnihilator_dualAnnihilator (W : Subspace K V) :
    W.map (Module.Dual.eval K V) ≤ W.dualAnnihilator.dualAnnihilator :=
  map_le_iff_le_comap.mpr (comap_dualAnnihilator_dualAnnihilator W).ge

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