le_dualAnnihilator_iff_le_dualCoannihilator

English

A restatement of the dual annihilator/coannihilator order relation in the complete lattice.

Русский

Переформулировка порядка дуального аннигилятора/коаннигилятор в полной решётке.

LaTeX

$$U ≤ V.dualAnnihilator ⇔ V ≤ U.dualCoannihilator$$

Lean4

theorem le_dualAnnihilator_iff_le_dualCoannihilator {U : Submodule R (Module.Dual R M)} {V : Submodule R M} :
    U ≤ V.dualAnnihilator ↔ V ≤ U.dualCoannihilator :=
  (dualAnnihilator_gc R M).le_iff_le

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