dualCoannihilator_dualAnnihilator_dualCoannihilator

English

For any submodule U of Module.Dual(R,M), (U.dualCoannihilator.dualAnnihilator.dualCoannihilator) = U.dualCoannihilator.

Русский

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

LaTeX

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

Lean4

theorem dualCoannihilator_dualAnnihilator_dualCoannihilator (U : Submodule R (Module.Dual R M)) :
    U.dualCoannihilator.dualAnnihilator.dualCoannihilator = U.dualCoannihilator :=
  (dualAnnihilator_gc R M).u_l_u_eq_u U

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