toSubMulAction_mono

Mathlib.Algebra.Module.Submodule.Basic

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

English

If p ≤ q then toSubMulAction(p) ≤ toSubMulAction(q).

Русский

Если p ⊆ q, то toSubMulAction(p) ⊆ toSubMulAction(q).

LaTeX

$$$p \le q \Rightarrow toSubMulAction(p) \le toSubMulAction(q)$$$

Lean4

@[mono]
theorem toSubMulAction_mono : Monotone (toSubMulAction : Submodule R M → SubMulAction R M) :=
  toSubMulAction_strictMono.monotone

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

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

Разделы

Аффилиация

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