mem_toList_iff — Mathlib

English

An element y belongs to toList p x exactly when x and y are in the same cycle of p and x is in the support of p.

Русский

Элемент y принадлежит toList p x тогда и только тогда, когда x и y лежат в одном цикле p и x принадлежит к поддержке p.

LaTeX

$$$$y \in toList\ p\ x \iff (p.SameCycle\ x\ y) \land (x \in p.\mathrm{support}).$$$$

Lean4

theorem mem_toList_iff {y : α} : y ∈ toList p x ↔ SameCycle p x y ∧ x ∈ p.support :=
  by
  simp only [toList, mem_iterate, iterate_eq_pow, eq_comm (a := y)]
  constructor
  · rintro ⟨n, hx, rfl⟩
    refine ⟨⟨n, rfl⟩, ?_⟩
    contrapose! hx
    rw [← support_cycleOf_eq_nil_iff] at hx
    simp [hx]
  · rintro ⟨h, hx⟩
    simpa using h.exists_pow_eq_of_mem_support hx

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