subsingleton_eq_refl

Mathlib.Logic.Equiv.Defs

URI: https://scilib.ai/kg/mathlib#Equiv.Perm.subsingleton_eq_refl

English

If α is Subsingleton, then any e ∈ Equiv.Perm α is equal to the identity permutation.

Русский

Если α пододномен, тогда любой e ∈ Equiv.Perm α равен тождественной перестановке.

LaTeX

$$$\forall e:\mathrm{Equiv.Perm} \alpha,\ e = \mathrm{Equiv.refl} \alpha$$$

Lean4

theorem subsingleton_eq_refl [Subsingleton α] (e : Perm α) : e = Equiv.refl α :=
  Subsingleton.elim _ _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru