trans_swap_trans_symm — Mathlib

English

Let e be a bijection α ≃ β. Then (e.trans (swap a b)).trans e.symm equals the swap of e.symm a and e.symm b.

Русский

Пусть e — биекция α ≃ β. Тогда (e.trans (swap a b)).trans e.symm равно перестановке swap( e.symm a, e.symm b ).

LaTeX

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

Lean4

@[simp]
theorem trans_swap_trans_symm [DecidableEq β] (a b : β) (e : α ≃ β) :
    (e.trans (swap a b)).trans e.symm = swap (e.symm a) (e.symm b) :=
  symm_trans_swap_trans a b e.symm

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