dualAnnihilator_dualCoannihilator_eq

English

For a subspace W of a vector space V, the double dual annihilator dualCoannihilator equals W.

Русский

Для подпространства W пространства V двойной аннигилятор совпадает с W.

LaTeX

$$W.dualAnnihilator.dualCoannihilator = W$$

Lean4

@[simp]
theorem dualAnnihilator_dualCoannihilator_eq {W : Subspace K V} : W.dualAnnihilator.dualCoannihilator = W :=
  by
  refine le_antisymm (fun v ↦ Function.mtr ?_) (le_dualAnnihilator_dualCoannihilator _)
  simp only [mem_dualAnnihilator, mem_dualCoannihilator]
  rw [← Quotient.mk_eq_zero W, ← Module.forall_dual_apply_eq_zero_iff K]
  push_neg
  refine fun ⟨φ, hφ⟩ ↦ ⟨φ.comp W.mkQ, fun w hw ↦ ?_, hφ⟩
  rw [comp_apply, mkQ_apply, (Quotient.mk_eq_zero W).mpr hw, φ.map_zero]
    -- exact elaborates slowly

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