coe_subsingleton — Mathlib

English

If α is a subsingleton, any permutation e of α acts as the identity on α.

Русский

Если α является одиночным по элементам (subsingleton), любая перестановка e над α действует как тождественная функция.

LaTeX

$$$[\\text{Subsingleton}(\\alpha)] \\Rightarrow (e:\\mathrm{Perm}(\\alpha)):(e:\\alpha\\to\\alpha)=\\mathrm{id}.$$$

Lean4

/-- This cannot be a `simp` lemmas as it incorrectly matches against `e : α ≃ synonym α`, when
`synonym α` is semireducible. This makes a mess of `Multiplicative.ofAdd` etc. -/
theorem coe_subsingleton {α : Type*} [Subsingleton α] (e : Perm α) : (e : α → α) = id := by
  rw [Perm.subsingleton_eq_refl e, coe_refl]

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