map_injective_of_injective — Mathlib

English

If f is injective, then the induced map on submodules p ↦ map f p is injective: distinct submodules have distinct images.

Русский

Если f инъективен, то индуцированное отображение подмодулов p ↦ p.map f инъективно: различные подмодули дают различные образы.

LaTeX

$$$\forall p\, q:\, Submodule\; R\; M,\ map\ f\ p = map\ f\ q \rightarrow p = q$$$

Lean4

theorem map_injective_of_injective : Function.Injective (map f) :=
  (gciMapComap hf).l_injective

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