swap_mul_eq_mul_swap — Mathlib

English

Conjugating a permutation by a swap behaves as expected: the swapped image of swapping x and y under f equals swapping their images under f and then applying f.

Русский

Свободная конъюгация перестановки через замены переставляет пары по ожидаемому правилу.

LaTeX

$$$ \\mathrm{swap}(f(x), f(y)) = f \\circ \\mathrm{swap}(x,y) \\circ f^{-1} $$$

Lean4

theorem swap_mul_eq_mul_swap (f : Perm α) (x y : α) : swap x y * f = f * swap (f⁻¹ x) (f⁻¹ y) :=
  Equiv.ext fun z => by
    simp only [Perm.mul_apply, swap_apply_def]
    split_ifs <;> simp_all only [Perm.apply_inv_self, Perm.eq_inv_iff_eq, not_true]

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