le_comap_map

Mathlib.RingTheory.Ideal.Maps

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

English

There is a dual relation: map f I ≤ K iff I ≤ comap f K.

Русский

Существует двумерная связь: map f I ≤ K тогда и только тогда I ≤ comap f K.

LaTeX

$$$ I \le K.comap f \Rightarrow I.map f ≤ K $$$

Lean4

theorem le_comap_map : I ≤ (I.map f).comap f :=
  (gc_map_comap f).le_u_l _

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

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

Разделы

Аффилиация

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