carrier — Mathlib

English

For any conjugacy class a in α, the carrier of a is the underlying set of elements of α that lie in that class.

Русский

Для любого конъюгированного класса a в α носитель a является множеством элементов α, принадлежащих этому классу.

LaTeX

$$$\mathrm{carrier}(a) = \{ x \in \alpha \mid \mathrm{ConjClasses.mk}(x) = a \}$$$

Lean4

/-- Given a conjugacy class `a`, `carrier a` is the set it represents. -/
def carrier : ConjClasses α → Set α :=
  Quotient.lift conjugatesOf fun (_ : α) _ ab => IsConj.conjugatesOf_eq ab

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