dualAnnihilator_iSup_eq — Mathlib

English

For a family of submodules U(i), the dual annihilator of their supremum equals the infimum of their dual annihilators: (⨆ i, U(i)).dualAnnihilator = ⨅ i, (U(i)).dualAnnihilator.

Русский

Для семейства подмодулей U(i) выполняется: (⨆ i, U(i)).dualAnnihilator = ⨅ i, (U(i)).dualAnnihilator.

LaTeX

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

Lean4

theorem dualAnnihilator_iSup_eq {ι : Sort*} (U : ι → Submodule R M) :
    (⨆ i : ι, U i).dualAnnihilator = ⨅ i : ι, (U i).dualAnnihilator :=
  (dualAnnihilator_gc R M).l_iSup

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