dualCoannihilator_iSup_eq — Mathlib

English

Similarly, for submodules U(i) of Module.Dual(R,M), the dual coannihilator of the supremum equals the infimum of the dual coannihilators: (⨆ i, U(i)).dualCoannihilator = ⨅ i, (U(i)).dualCoannihilator.

Русский

Аналогично: (⨆ i, U(i)).dualCoannihilator = ⨅ i, (U(i)).dualCoannihilator.

LaTeX

$$$ \\big(\\big\\vee_{i} U(i)\\big).dualCoannihilator = \\bigwedge_{i} (U(i)).dualCoannihilator $$$

Lean4

theorem dualCoannihilator_iSup_eq {ι : Sort*} (U : ι → Submodule R (Module.Dual R M)) :
    (⨆ i : ι, U i).dualCoannihilator = ⨅ i : ι, (U i).dualCoannihilator :=
  (dualAnnihilator_gc R M).u_iInf

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