normalClosure_le_normal — Mathlib

English

If N is a normal subgroup with s ⊆ N, then normalClosure(s) ≤ N.

Русский

Если N — нормальная подгруппа и s ⊆ N, то normalClosure(s) ≤ N.

LaTeX

$$$ s \subseteq N \Rightarrow \mathrm{normalClosure}(s) \le N $$$

Lean4

/-- The normal closure of `s` is the smallest normal subgroup containing `s`. -/
theorem normalClosure_le_normal {N : Subgroup G} [N.Normal] (h : s ⊆ N) : normalClosure s ≤ N :=
  by
  intro a w
  refine closure_induction (fun x hx => ?_) ?_ (fun x y _ _ ihx ihy => ?_) (fun x _ ihx => ?_) w
  · exact conjugatesOfSet_subset h hx
  · exact one_mem _
  · exact mul_mem ihx ihy
  · exact inv_mem ihx

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