mk_surjective — Mathlib

English

The map ConjClasses.mk: α → ConjClasses α is surjective: every conjugacy class has a representative.

Русский

Отображение ConjClasses.mk: α → ConjClasses α сюръективно: каждый класс сопряжённости имеет представителя.

LaTeX

$$$\text{ConjClasses.mk}: \alpha \to \mathrm{ConjClasses}(\alpha)$ is surjective; i.e., ∀ A ∈ ConjClasses(α), ∃ a ∈ α, ConjClasses.mk(a) = A.$$

Lean4

theorem mk_surjective : Function.Surjective (@ConjClasses.mk α _) :=
  forall_isConj.2 fun a => ⟨a, rfl⟩

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