comap_dualAnnihilator_dualAnnihilator

English

Let W be a subspace of a vector space V over a field K. The double annihilator of W coincides with W under the canonical embedding into the double dual; equivalently, W equals the set of v in V such that every functional vanishing on W also vanishes at v.

Русский

Пусть W является подпространством V над полем K. Двойной аннигилятор W совпадает с W после естественного отображения V в двойной двойной пространств; то есть W = { v ∈ V : φ(v) = 0 для всех φ ∈ W^⊥ }.

LaTeX

$$$j(W) = (W^{\perp})^{\perp}$, где $j: V \to V^{**}$ есть оценочное отображение.$$

Lean4

theorem comap_dualAnnihilator_dualAnnihilator (W : Subspace K V) :
    W.dualAnnihilator.dualAnnihilator.comap (Module.Dual.eval K V) = W := by ext;
  rw [Iff.comm, ← forall_mem_dualAnnihilator_apply_eq_zero_iff]; simp

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