map_mono — Mathlib

English

If I ⊆ J are two-sided ideals of R and f is a suitable mapping, then map f I ⊆ map f J.

Русский

Пусть I ⊆ J — двусторонние идеалы кольца R, и пусть отображение f ведет иделы в кольце-образе. Тогда образ I под действием f ⊆ образ J под действием f.

LaTeX

$$$I \\le J \\Rightarrow \\operatorname{map}_f(I) \\le \\operatorname{map}_f(J)$$$

Lean4

theorem map_mono {I J : TwoSidedIdeal R} (h : I ≤ J) : map f I ≤ map f J :=
  span_mono <| Set.image_mono h

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