dualCoannihilator_sup_eq — Mathlib

English

For submodules U,V of Module.Dual(R,M), the join of their dual coannihilators equals the meet of their dual annihilators: (U ⊔ V).dualCoannihilator = U.dualCoannihilator ⊓ V.dualCoannihilator.

Русский

Для U,V ⊆ M в дуальном модуле выполняется: (U ⊔ V).dualCoannihilator = U.dualCoannihilator ⊓ V.dualCoannihilator.

LaTeX

$$$ (U \\or V).dualCoannihilator = U.dualCoannihilator \\cap V.dualCoannihilator $$$

Lean4

theorem dualCoannihilator_sup_eq (U V : Submodule R (Module.Dual R M)) :
    (U ⊔ V).dualCoannihilator = U.dualCoannihilator ⊓ V.dualCoannihilator :=
  (dualAnnihilator_gc R M).u_inf

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