English
Let p be a natural number, G a group, and H, K subgroups of G such that H and K are p-subgroups and K is normal in G. Then the subgroup generated by H and K (their join) is a p-subgroup.
Русский
Пусть p — натуральное число, G — группа, H и K — подгруппы G такие, что H и K являются p-подгруппами, а K нормальна в G. Тогда порожденная суммой H и K подгруппа является p-подгруппой.
LaTeX
$$$\\text{If } H, K \\le G \\text{ are subgroups with } H \\text{ and } K \\text{ are } p\\text{-subgroups and } K \\trianglelefteq G, \\\\ \\text{then } \\langle H \\cup K \\rangle \\text{ is a } p\\text{-subgroup.}$$$
Lean4
theorem to_sup_of_normal_right {H K : Subgroup G} (hH : IsPGroup p H) (hK : IsPGroup p K) [K.Normal] :
IsPGroup p (H ⊔ K : Subgroup G) :=
by
rw [← QuotientGroup.ker_mk' K, ← Subgroup.comap_map_eq]
apply (hH.map (QuotientGroup.mk' K)).comap_of_ker_isPGroup
rwa [QuotientGroup.ker_mk']
