length_toList — Mathlib

English

The length of the list produced by toList p x equals the card of the support of the cycle containing x.

Русский

Длина списка, полученного как toList p x, равна кардиналу множества переносов цикла cycleOf p x.

LaTeX

$$$$\forall \alpha\ [\mathrm{Fintype}\ \alpha] [\mathrm{DecidableEq}\ \alpha] (p : \mathrm{Equiv.Perm}\ \alpha) (x : \alpha),\ \mathrm{length}(\mathrm{toList}\ p\ x) = (\mathrm{cycleOf}\ p\ x).\mathrm{support}.\mathrm{card}.$$$$

Lean4

@[simp]
theorem length_toList : length (toList p x) = (cycleOf p x).support.card := by simp [toList]

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