pow_apply_mem_toList_iff_mem_support

English

If f is a cycle, then the corresponding toCycle construction yields a nodup cycle.

Русский

Если f — цикл, то полученная конструкция toCycle дает цикл без повторений.

LaTeX

$$$$\text{If } f:\mathrm{Perm}\ \alpha \text{ is a cycle, then } (\mathrm{toCycle}\ f\ hf).\mathrm{Nodup}.$$$$

Lean4

theorem pow_apply_mem_toList_iff_mem_support {n : ℕ} : (p ^ n) x ∈ p.toList x ↔ x ∈ p.support :=
  by
  rw [mem_toList_iff, and_iff_right_iff_imp]
  refine fun _ => SameCycle.symm ?_
  rw [sameCycle_pow_left]

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