toList_one — Mathlib

English

Let α be a finite type with decidable equality. For every x in α, the list produced by applying the identity permutation to x is empty.

Русский

Пусть α — конечный тип с разрешенным равенством. Для каждого x ∈ α список, получаемый приложением тождественной перестановки к x, равен пустому списку.

LaTeX

$$$$\forall \alpha\ [\mathrm{Fintype}\ \alpha]\ [\mathrm{DecidableEq}\ \alpha],\ \forall x:\alpha,\ \operatorname{toList}(1:\mathrm{Perm}\ \alpha)\,x = [].$$$$

Lean4

@[simp]
theorem toList_one : toList (1 : Perm α) x = [] := by simp [toList, cycleOf_one]

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