toAddSubmonoid_mono

Mathlib.Algebra.Module.Submodule.Basic

URI: https://scilib.ai/kg/mathlib#Submodule.toAddSubmonoid_mono

English

If p ≤ q then p.toAddSubmonoid ≤ q.toAddSubmonoid.

Русский

Если p ⊆ q, то p.toAddSubmonoid ⊆ q.toAddSubmonoid.

LaTeX

$$$p \le q \Rightarrow p.toAddSubmonoid \le q.toAddSubmonoid$$$

Lean4

@[mono]
theorem toAddSubmonoid_mono : Monotone (toAddSubmonoid : Submodule R M → AddSubmonoid M) :=
  toAddSubmonoid_strictMono.monotone

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru