map_le_of_le_comap

Mathlib.RingTheory.Ideal.Maps

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

English

If I ≤ comap f K, then map f I ≤ K.

Русский

Если I ≤ comap f K, то map f I ≤ K.

LaTeX

$$$ I \le \operatorname{comap} f K \Rightarrow \operatorname{map} f I \le K $$$

Lean4

theorem map_le_of_le_comap : I ≤ K.comap f → I.map f ≤ K :=
  (gc_map_comap f).l_le

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

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

Разделы

Аффилиация

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