map_mono

Mathlib.RingTheory.Ideal.Maps

URI: https://scilib.ai/kg/mathlib#Ideal.map_mono

English

If I ≤ J, then map f I ≤ map f J.

Русский

Если I ⊆ J, то map f I ⊆ map f J.

LaTeX

$$$I \\le J \\Rightarrow I.map f \\le J.map f$$$

Lean4

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

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

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

Разделы

Аффилиация

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