sameCycle_apply_right — Mathlib

English

Applying the right argument under a permutation preserves SameCycle after swapping with commutation.

Русский

Применение справа в рамках перестановки сохраняет отношение SameCycle после перестановки.

LaTeX

$$$\\forall f:\\mathrm{Equiv.Perm}(\\alpha),\\; \\forall x,y:\\alpha,\\ SameCycle\\,f\\,x\\,(f\\,y) \\iff SameCycle\\,f\\,x\\,y.$$$

Lean4

@[simp]
theorem sameCycle_apply_right : SameCycle f x (f y) ↔ SameCycle f x y := by
  rw [sameCycle_comm, sameCycle_apply_left, sameCycle_comm]

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