map_mono — Mathlib

English

If p ⊆ p' are submodules of M and f is a semilinear map, then the image preserves inclusion: map f p ⊆ map f p'.

Русский

Если p ⊆ p' — подмодули M и задано отображение f, то образ подмодуля p под f включён в образ p' под f: map f p ⊆ map f p'.

LaTeX

$$$p \\subseteq p' \\Rightarrow map\\,f\\,p \\subseteq map\\,f\\,p'$$

Lean4

@[gcongr]
theorem map_mono {f : F} {p p' : Submodule R M} : p ≤ p' → map f p ≤ map f p' :=
  image_mono

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