dualAnnihilator_dualCoannihilator_dualAnnihilator

English

For any submodule U of M, taking dual, then dual coannihilator, then dual again returns to the original dual annihilator: (U.dualAnnihilator.dualCoannihilator.dualAnnihilator) = U.dualAnnihilator.

Русский

Для любого подмодуля U пространства M справедлива тройная дуализация: (U.dualAnnihilator.dualCoannihilator.dualAnnihilator) = U.dualAnnihilator.

LaTeX

$$$ U.dualAnnihilator.dualCoannihilator.dualAnnihilator = U.dualAnnihilator $$$

Lean4

theorem dualAnnihilator_dualCoannihilator_dualAnnihilator (U : Submodule R M) :
    U.dualAnnihilator.dualCoannihilator.dualAnnihilator = U.dualAnnihilator :=
  (dualAnnihilator_gc R M).l_u_l_eq_l U

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