toCycle_eq_toList — Mathlib

English

If f is a cyclic permutation and x is not fixed by f, then the toCycle construction equals the toList starting at x.

Русский

Если f — цикл перестановки и x не зафиксирован f, то toCycle f hf = toList f x.

LaTeX

$$$$\text{If } f:\mathrm{Perm}\ α \text{ IsCycle } hf\text{ and } f x \neq x,\ \mathrm{toCycle}\ f hf = \mathrm{toList}\ f x.$$$$

Lean4

theorem toCycle_eq_toList (f : Perm α) (hf : IsCycle f) (x : α) (hx : f x ≠ x) : toCycle f hf = toList f x :=
  by
  have key : (Finset.univ : Finset α).val = x ::ₘ Finset.univ.val.erase x := by simp
  rw [toCycle, key]
  simp [hx]

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