dualAnnihilator_sup_eq — Mathlib

English

For submodules U,V ⊆ M, the dual annihilator of the join equals the meet of dual annihilators: (U ⊔ V).dualAnnihilator = U.dualAnnihilator ⊓ V.dualAnnihilator.

Русский

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

LaTeX

$$$ (U \\sqcup V).dualAnnihilator = U.dualAnnihilator \\cap V.dualAnnihilator $$$

Lean4

theorem dualAnnihilator_sup_eq (U V : Submodule R M) :
    (U ⊔ V).dualAnnihilator = U.dualAnnihilator ⊓ V.dualAnnihilator :=
  (dualAnnihilator_gc R M).l_sup

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