Group_Generated_by_Normal_Intersection_is_Normal
Provedgenerated-subgroupgroup-theorynormal-subgroupproofwiki
If {N_i} is a family of normal subgroups of G, then the subgroup generated by their union (the supremum) is also normal.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Group_Generated_by_Normal_Intersection_is_Normal {G : Type _} [Group G] {I : Type _} (N : I → Subgroup G) (hN : ∀ i, (N i).Normal) : (⨆ i, N i).Normal := by sorrySource