mem_support_cycleOf_iff' — Mathlib

English

If f x ≠ x, then y lies in the support of f.cycleOf x exactly when y is in the same cycle as x under f.

Русский

Если f x ≠ x, тогда y принадлежит поддержке cycleOf x тогда и только тогда, когда y в той же самой цепи, что и x по f.

LaTeX

$$$(cycleOf f x).\\\\support \\\\ni y \\\\iff SameCycle f x y$$$

Lean4

theorem mem_support_cycleOf_iff' (hx : f x ≠ x) [DecidableEq α] [Fintype α] :
    y ∈ support (f.cycleOf x) ↔ SameCycle f x y :=
  mem_support_cycleOf_iff'_aux hx

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