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 H 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-подгруппы, а H нормальна в G. Тогда подгруппа, порождаемая H и K (их сумма), является p-подгруппой.
LaTeX
$$$\\text{If } H, K \\le G \\text{ are subgroups with } H, K \\text{ p-subgroups and } H \\trianglelefteq G, \\\\ \\text{then } \\langle H \\cup K \\rangle \\text{ is a } p\\text{-subgroup.}$$$
Lean4
theorem to_sup_of_normal_left {H K : Subgroup G} (hH : IsPGroup p H) (hK : IsPGroup p K) [H.Normal] :
IsPGroup p (H ⊔ K : Subgroup G) :=
sup_comm H K ▸ to_sup_of_normal_right hK hH
