comap_le_map_of_inv_on

Mathlib.RingTheory.Ideal.Maps

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

← MathLib Explorer

English

If K ≤ L then comap f K ≤ comap f L.

Русский

Если K ⊆ L, то comap f K ⊆ comap f L.

LaTeX

$$$ K \le L \Rightarrow \operatorname{comap} f K \le \operatorname{comap} f L $$$

Lean4

theorem comap_le_map_of_inv_on [RingHomClass F R S] (g : G) (I : Ideal S) (hf : Set.LeftInvOn g f (f ⁻¹' I)) :
    I.comap f ≤ I.map g := fun x (hx : f x ∈ I) => hf hx ▸ Ideal.mem_map_of_mem g hx

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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