le_dualCoannihilator_dualAnnihilator

English

The dual coannihilator of the dual annihilator of a submodule equals the dual annihilator: U.dualAnnihilator.dualCoannihilator = U.dualAnnihilator.

Русский

Дуальный коаннигильятор дуального аннигиляторa подмодуля совпадает с дуальным аннигилятором: U.dualAnnihilator.dualCoannihilator = U.dualAnnihilator.

LaTeX

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

Lean4

theorem le_dualCoannihilator_dualAnnihilator (U : Submodule R (Module.Dual R M)) :
    U ≤ U.dualCoannihilator.dualAnnihilator :=
  (dualAnnihilator_gc R M).l_u_le U

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