comap_inclusion_subgroupOf — Mathlib

English

If K1 ≤ K2 are subgroups of G, then (H.subgroupOf K2).comap (inclusion h) equals H.subgroupOf K1, where h is the inclusion map corresponding to h: K1 ≤ K2.

Русский

Если K1 ≤ K2 — подгруппы G, то (H.subgroupOf K2).comap (inclusion h) = H.subgroupOf K1, где h — включение соответствующее K1 ≤ K2.

LaTeX

$$$ (H.subgroupOf K_2).comap (\\mathrm{inclusion}\\ h) = H.subgroupOf K_1 $$$

Lean4

@[to_additive (attr := simp)]
theorem comap_inclusion_subgroupOf {K₁ K₂ : Subgroup G} (h : K₁ ≤ K₂) (H : Subgroup G) :
    (H.subgroupOf K₂).comap (inclusion h) = H.subgroupOf K₁ :=
  rfl

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