comap_subtype — Mathlib

English

For subgroups H ≤ G and K ≤ G, the comap of H.subgroupOf K along the inclusion map equals H.subgroupOf K itself; i.e., pulling back along inclusion recovers the same subgroup of K.

Русский

Для подгрупп H ≤ G и K ≤ G проекция через вложение восстанавливает H.subgroupOf K.

LaTeX

$$$(H.subgroupOf K) \\text{ comap incl } = H.subgroupOf K$$$

Lean4

@[to_additive (attr := simp)]
theorem comap_subtype (H K : Subgroup G) : H.comap K.subtype = H.subgroupOf K :=
  rfl

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