le_comap_mk' — Mathlib

English

The comap of a Mk' map preserves subgroup ordering: for subgroups N ≤ M, the comap of mk' by N to a subgroup H respects the join with N and manages normal subgroups accordingly.

Русский

Сохранение порядка подгрупп через отображение mk': для N ≤ M отображение сохраняет соединение и нормальные подгруппы.

LaTeX

$$$N \\le M \\ \\Rightarrow\\ Subgroup.comap(\\mathrm{mk}' N)(H) \\le \\cdot$$$

Lean4

@[to_additive]
theorem le_comap_mk' (N : Subgroup G) [N.Normal] (H : Subgroup (G ⧸ N)) : N ≤ Subgroup.comap (QuotientGroup.mk' N) H :=
  by simpa using Subgroup.comap_mono (f := mk' N) bot_le

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