mem_conjugatesOfSet_iff — Mathlib

English

Let s be a subset of a group G. An element x belongs to the set of conjugates of s if and only if x is a conjugate of some element of s.

Русский

Пусть s—множество группы G. Элемент x принадлежит множеству конъюгатов множества s тогда и только тогда, когда x является конъюгатом некоторого элемента из s.

LaTeX

$$$ x \in \mathrm{conjugatesOfSet}(s) \iff \exists a \in s, \exists g \in G, g a g^{-1} = x $$$

Lean4

theorem mem_conjugatesOfSet_iff {x : G} : x ∈ conjugatesOfSet s ↔ ∃ a ∈ s, IsConj a x :=
  by
  rw [conjugatesOfSet, Set.mem_iUnion₂]
  simp only [conjugatesOf, isConj_iff, Set.mem_setOf_eq, exists_prop]

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