inf_subgroupOf_inf_normal_of_left

English

Let A' ≤ A with A' normal in A and B a subgroup of G. Then (A' ∩ B) is normal in (A ∩ B).

Русский

Пусть A' ≤ A и A' нормальна в A, и B — подгруппа G. Тогда A' ∩ B нормальна в A ∩ B.

LaTeX

$$((A' ∩ B).Normal) in (A ∩ B)$$

Lean4

@[to_additive]
theorem inf_subgroupOf_inf_normal_of_left {A' A : Subgroup G} (B : Subgroup G) [hN : (A'.subgroupOf A).Normal] :
    ((A' ⊓ B).subgroupOf (A ⊓ B)).Normal :=
  by
  rw [normal_subgroupOf_iff_le_normalizer_inf] at hN ⊢
  rw [inf_inf_inf_comm, inf_idem]
  exact le_trans (inf_le_inf hN B.le_normalizer) (inf_normalizer_le_normalizer_inf)

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