comap_le_comap

Mathlib.RingTheory.TwoSidedIdeal.Operations

URI: https://scilib.ai/kg/mathlib#TwoSidedIdeal.comap_le_comap

English

If I ⊆ J are two-sided ideals of S, then comap f I ⊆ comap f J.

Русский

Пусть I ⊆ J — двусторонние идеалы кольца S, тогда обратный образ по f сохраняет включение.

LaTeX

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

Lean4

theorem comap_le_comap {I J : TwoSidedIdeal S} (h : I ≤ J) : comap f I ≤ comap f J :=
  (comap f).monotone h

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

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

Разделы

Аффилиация

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