subgroupComap_surjective_of_surjective

English

If f: G →* G' is surjective, then the induced subgroup map f.subgroupComap H' is surjective for every subgroup H' ⊆ G'.

Русский

Если f: G →* G' сюръективен, то соответствующее отображение подгрупп f.subgroupComap H' сюръективно на H'.

LaTeX

$$Surjective(f.subgroupComap(H')) given Surjective(f)$$

Lean4

@[to_additive]
theorem subgroupComap_surjective_of_surjective (f : G →* G') (H' : Subgroup G') (hf : Surjective f) :
    Surjective (f.subgroupComap H') :=
  f.submonoidComap_surjective_of_surjective H'.toSubmonoid hf

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