dualCoannihilator_anti — Mathlib

English

If U ≤ V are submodules of Module.Dual(R,M), then V.dualCoannihilator ≤ U.dualCoannihilator.

Русский

Если U ⊆ V применимо к дуальному модулю, то V.dualCoannihilator ⊆ U.dualCoannihilator.

LaTeX

$$$ U \\le V \\;\\Rightarrow\\; V.dualCoannihilator \\le U.dualCoannihilator $$$

Lean4

@[mono]
theorem dualCoannihilator_anti {U V : Submodule R (Module.Dual R M)} (hUV : U ≤ V) :
    V.dualCoannihilator ≤ U.dualCoannihilator :=
  (dualAnnihilator_gc R M).monotone_u hUV

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