toAddSubgroup_mono — Mathlib

English

The map from submodules to AddSubgroups is monotone; in particular, if p ≤ p' then the corresponding AddSubgroups satisfy p.toAddSubgroup ≤ p'.toAddSubgroup.

Русский

Отображение подмодулов в аддитивные подгруппы монотонно: если p ≤ p', то соответствующие AddSubgroup удовлетворяют p.toAddSubgroup ≤ p'.toAddSubgroup.

LaTeX

$$$p \\le p' \\Rightarrow p^{\\text{AddSubgroup}} \\le (p')^{\\text{AddSubgroup}}$$$

Lean4

@[mono]
theorem toAddSubgroup_mono : Monotone (toAddSubgroup : Submodule R M → AddSubgroup M) :=
  toAddSubgroup_strictMono.monotone

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