le_comap_of_map_le

Mathlib.RingTheory.Ideal.Maps

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

English

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

Русский

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

LaTeX

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

Lean4

theorem le_comap_of_map_le : I.map f ≤ K → I ≤ K.comap f :=
  (gc_map_comap f).le_u

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

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

Разделы

Аффилиация

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