map_strictMono_of_injective

Mathlib.Algebra.Module.Submodule.Map

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

English

The map on submodules is strictly monotone: if p < q then map f p < map f q.

Русский

Отображение подмодулов строго монотонно по включению: если p < q, то p.map f < q.map f.

LaTeX

$$$\forall p,q:\, Submodule\; R\; M,\ p < q\Rightarrow p.map f < q.map f$$$

Lean4

theorem map_strictMono_of_injective : StrictMono (map f) :=
  (gciMapComap hf).strictMono_l

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

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

Разделы

Аффилиация

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