sameCycle_inv — Mathlib

English

For any permutation f on α, x and y lie in the same cycle of f⁻¹ if and only if they lie in the same cycle of f.

Русский

Для перестановки f на α точки x и y лежат в одной и той же цикле f⁻¹ тогда и только тогда, когда они лежат в одной и той же цикле f.

LaTeX

$$$\\forall f:\\mathrm{Perm}(\\alpha),\\; \\forall x,y\\in\\alpha,\\; (f^{-1} \\text{ SameCycle } x y) \\iff (f \\text{ SameCycle } x y).$$$

Lean4

@[simp]
theorem sameCycle_inv : SameCycle f⁻¹ x y ↔ SameCycle f x y :=
  (Equiv.neg _).exists_congr_left.trans <| by simp [SameCycle]

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