conj_mem_conjugatesOfSet — Mathlib

English

The set conjugatesOfSet s is closed under conjugation: if x ∈ conjugatesOfSet s and c ∈ G, then c x c^{-1} ∈ conjugatesOfSet s.

Русский

Множество conjugatesOfSet s замкнуто относительно конъюгации: если x ∈ conjugatesOfSet s и c ∈ G, то c x c^{-1} ∈ conjugatesOfSet s.

LaTeX

$$$ x \in \mathrm{conjugatesOfSet}(s) \Rightarrow c x c^{-1} \in \mathrm{conjugatesOfSet}(s) $$$

Lean4

/-- The set of conjugates of `s` is closed under conjugation. -/
theorem conj_mem_conjugatesOfSet {x c : G} : x ∈ conjugatesOfSet s → c * x * c⁻¹ ∈ conjugatesOfSet s := fun H =>
  by
  rcases mem_conjugatesOfSet_iff.1 H with ⟨a, h₁, h₂⟩
  exact mem_conjugatesOfSet_iff.2 ⟨a, h₁, h₂.trans (isConj_iff.2 ⟨c, rfl⟩)⟩

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