toList — Mathlib

English

For l, h nodup, and x ∈ l, formPerm l h x equals next l h x hx.

Русский

Для l, h нодуп и x ∈ l, formPerm l h x равно следующему элементу.

LaTeX

$$$\\text{formPerm\\_apply\\_mem\\_eq\\_next}(h, x, hx) :\\; \\text{formPerm } l h x = \\text{next } l h x hx$$$

Lean4

/-- `Equiv.Perm.toList (f : Perm α) (x : α)` generates the list `[x, f x, f (f x), ...]`
until looping. That means when `f x = x`, `toList f x = []`.
-/
def toList : List α :=
  List.iterate p x (cycleOf p x).support.card

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