conjugatesOfSet_subset — Mathlib

English

If s is contained in a normal subgroup N, then all conjugates of elements of s lie in N.

Русский

Если s ⊆ N, где N нормальная, то конъюгаты элементов s лежат в N.

LaTeX

$$$ s \subseteq N \Rightarrow \mathrm{conjugatesOfSet}(s) \subseteq N $$$

Lean4

theorem conjugatesOfSet_subset {s : Set G} {N : Subgroup G} [N.Normal] (h : s ⊆ N) : conjugatesOfSet s ⊆ N :=
  Set.iUnion₂_subset fun _x H => conjugates_subset_normal (h H)

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