symm_trans_swap_trans — Mathlib

English

Let e be a bijection α ≃ β. Then the conjugate of the swap on α by e equals the swap on β: e^{-1} ∘ swap(a,b) ∘ e = swap(e^{-1}(a), e^{-1}(b)).

Русский

Пусть e — биекция α ≃ β. Тогда сопряжение транспозиции swap(a,b) через e даёт транспозицию между e^{-1}(a) и e^{-1}(b) на β.

LaTeX

$$$e^{-1} \circ \mathrm{swap}(a,b) \circ e = \mathrm{swap}(e^{-1}(a), e^{-1}(b))$$$

Lean4

@[simp]
theorem symm_trans_swap_trans [DecidableEq β] (a b : α) (e : α ≃ β) :
    (e.symm.trans (swap a b)).trans e = swap (e a) (e b) :=
  Equiv.ext fun x => by
    have : ∀ a, e.symm x = a ↔ x = e a := fun a => by grind
    simp only [trans_apply, swap_apply_def, this]
    split_ifs <;> simp

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