toSubgroup_comap — Mathlib

English

The Subgroup underlying comap matches the Subgroup comap of H by f: (H.comap f hf).toSubgroup = Subgroup.comap f H.toSubgroup.

Русский

Подгруппа, соответствующая предобразованию, совпадает с предобразованием подгруппы: (H.comap f hf).toSubgroup = Subgroup.comap f H.toSubgroup.

LaTeX

$$$$ (H^{\\mathrm{comap} f hf})^{\\mathrm{toSubgroup}} = \\mathrm{Subgroup.comap} f H^{\\mathrm{toSubgroup}}. $$$$

Lean4

@[to_additive (attr := simp, norm_cast)]
theorem toSubgroup_comap (H : OpenSubgroup N) (f : G →* N) (hf : Continuous f) :
    (H.comap f hf : Subgroup G) = (H : Subgroup N).comap f :=
  rfl

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