forall_mem_dualAnnihilator_apply_eq_zero_iff

English

Equality of dualCoannihilator and the original subspace holds for a reflexive module with dualities.

Русский

Равенство двойного коаннигилятора и исходного подпространства сохраняется в рефлексивном модуле.

LaTeX

$$Subspace.dualCoannihilator(W) = W$$

Lean4

theorem forall_mem_dualAnnihilator_apply_eq_zero_iff (W : Subspace K V) (v : V) :
    (∀ φ : Module.Dual K V, φ ∈ W.dualAnnihilator → φ v = 0) ↔ v ∈ W := by
  rw [← SetLike.ext_iff.mp dualAnnihilator_dualCoannihilator_eq v, mem_dualCoannihilator]

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