to_sup_of_normal_left' — Mathlib

English

Let H and K be p-subgroups of G with H normal in G and both p-subgroups. Then the join H ⊔ K is a p-subgroup.

Русский

Пусть H и K — p-подгруппы G, при этом H нормальна в G. Тогда сумма H ⊔ K — p-подгруппа.

LaTeX

$$$\text{If } H, K \le G \text{ are p-subgroups with } 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) (hHK : K ≤ H.normalizer) :
    IsPGroup p (H ⊔ K : Subgroup G) :=
  sup_comm H K ▸ to_sup_of_normal_right' hK hH hHK

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