orbit_eq_carrier_conjClasses — Mathlib

English

The orbit of g under ConjAct G equals the carrier of the conjugacy class of g.

Русский

Орбита g по действию сопряжения равна носителю класса сопряженности g.

LaTeX

$$$\operatorname{orbit}(\operatorname{ConjAct} G, g) = (\operatorname{ConjClasses.mk} g).\text{carrier}$$$

Lean4

theorem orbit_eq_carrier_conjClasses (g : G) : orbit (ConjAct G) g = (ConjClasses.mk g).carrier :=
  by
  ext h
  rw [ConjClasses.mem_carrier_iff_mk_eq, ConjClasses.mk_eq_mk_iff_isConj, mem_orbit_conjAct]

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