English
Let H and K be p-subgroups of G, with H ≤ K.normalizer. Then the join H ⊔ K is a p-subgroup.
Русский
Пусть H и K — p-подгруппы G, причем H ≤ N_G(K). Тогда сумма H ⊔ K — p-подгруппа.
LaTeX
$$$\text{If } H, K \le G \text{ are p-subgroups with } H \le N_G(K), \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) (hHK : H ≤ K.normalizer) :
IsPGroup p (H ⊔ K : Subgroup G) :=
let hHK' :=
to_sup_of_normal_right (hH.of_equiv (Subgroup.subgroupOfEquivOfLe hHK).symm)
(hK.of_equiv (Subgroup.subgroupOfEquivOfLe Subgroup.le_normalizer).symm)
((congr_arg (fun H : Subgroup K.normalizer => IsPGroup p H)
(Subgroup.sup_subgroupOf_eq hHK Subgroup.le_normalizer)).mp
hHK').of_equiv
(Subgroup.subgroupOfEquivOfLe (sup_le hHK Subgroup.le_normalizer))
