carrier_eq_preimage_mk — Mathlib

English

The carrier of a conjugacy class equals the preimage of the singleton {a} under the quotient map.

Русский

Носитель конъюгированного класса равен предобразу множества {a} под отображением-квадрификатором.

LaTeX

$$$\mathrm{carrier}(a) = \mathrm{mk}^{-1}\{ a \}$$$

Lean4

theorem carrier_eq_preimage_mk {a : ConjClasses α} : a.carrier = ConjClasses.mk ⁻¹' { a } :=
  Set.ext fun _ => mem_carrier_iff_mk_eq

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