comap_sup_comap_le

Mathlib.Algebra.Group.Subgroup.Map

URI: https://scilib.ai/kg/mathlib#Subgroup.comap_sup_comap_le

← MathLib Explorer

English

If H and K are subgroups of G and f: G → N is injective, then (H ⊓ K).map f = H.map f ⊓ K.map f.

Русский

Если H и K — подгруппы G, и f инъективен, то (H ⊓ K).map f = H.map f ⊓ K.map f.

LaTeX

$$$(H \\cap K).map f = H.map f \\cap K.map f.$$$

Lean4

@[to_additive]
theorem comap_sup_comap_le (H K : Subgroup N) (f : G →* N) : comap f H ⊔ comap f K ≤ comap f (H ⊔ K) :=
  Monotone.le_map_sup (fun _ _ => comap_mono) H K

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

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

Разделы

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

Аффилиация

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