getElem_toList — Mathlib

English

For n less than the length of toList p x, the nth element of toList p x equals (p^n) x.

Русский

Для n, меньшего длины toList p x, n-ый элемент списка равен (p^n) x.

LaTeX

$$$$\forall {\alpha} [Fintype \alpha] [DecidableEq \alpha] (p : Equiv.Perm \alpha) (x : \alpha) (n : \mathbb{N}),\ n < \mathrm{length}(\mathrm{toList}\ p\ x) \Rightarrow (\mathrm{toList}\ p\ x)[n] = (p^n) x.$$$$

Lean4

theorem getElem_toList (n : ℕ) (hn : n < length (toList p x)) : (toList p x)[n] = (p ^ n) x := by simp [toList]

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