normalClosure_subset_iff — Mathlib

English

The normal closure of s equals the infimum of all normal subgroups containing s.

Русский

Нормальное замыкание s равно наибольшему общему снизу (поглощение) всех нормальных подгрупп, содержащих s.

LaTeX

$$$ \mathrm{normalClosure}(s) = \bigwedge_{N \trianglelefteq G,\ s \subseteq N} N $$$

Lean4

theorem normalClosure_subset_iff {N : Subgroup G} [N.Normal] : s ⊆ N ↔ normalClosure s ≤ N :=
  ⟨normalClosure_le_normal, Set.Subset.trans subset_normalClosure⟩

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