le_dualAnnihilator_dualCoannihilator

English

For any submodule U of the dual space Module.Dual(R,M), U is contained in the dual annihilator of its dual coannihilator: U ≤ U.dualAnnihilator.dualCoannihilator.

Русский

Для любого подмодуля U подпространства дуального пространства: U ⊆ U.dualAnnihilator.dualCoannihilator.

LaTeX

$$$ U \\le U.dualAnnihilator.dualCoannihilator $$$

Lean4

theorem le_dualAnnihilator_dualCoannihilator (U : Submodule R M) : U ≤ U.dualAnnihilator.dualCoannihilator :=
  (dualAnnihilator_gc R M).le_u_l U

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