dualAnnihilator_anti — Mathlib

English

If U and V are submodules of M with U contained in V, then the dual annihilator reverses inclusion: V.dualAnnihilator ⊆ U.dualAnnihilator.

Русский

Пусть U ⊆ V — подмодули M. Тогда антисимметрично относительно двойного аннигилятора: V.dualAnnihilator ⊆ U.dualAnnihilator.

LaTeX

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

Lean4

@[mono]
theorem dualAnnihilator_anti {U V : Submodule R M} (hUV : U ≤ V) : V.dualAnnihilator ≤ U.dualAnnihilator :=
  (dualAnnihilator_gc R M).monotone_l hUV

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