exists_rep — Mathlib

English

Every conjugacy class has a representative: for any a ∈ ConjClasses α, there exists a0 ∈ α with ConjClasses.mk(a0) = a.

Русский

Каждый класс сопряжённости имеет представителя: для любого a ∈ ConjClasses α существует a0 ∈ α, такое что ConjClasses.mk(a0) = a.

LaTeX

$$$\forall a:\ConjClasses(\alpha), \exists a0:\alpha, \ConjClasses.mk(a0) = a$$$

Lean4

theorem exists_rep (a : ConjClasses α) : ∃ a0 : α, ConjClasses.mk a0 = a :=
  Quot.exists_rep a

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