English
For embeddings f, swap_comp asserts that swapping after applying f is the same as applying f after swapping inputs.
Русский
Соглашение swap_comp говорит, что перестановка после применения вложения равна применению вложения после перестановки входов.
LaTeX
$$$\\mathrm{swap}_{\\beta}(f x, f y) \\circ f = f \\circ \\mathrm{swap}_{\\alpha}(x,y)$$$
Lean4
theorem swap_comp {α β : Type*} [DecidableEq α] [DecidableEq β] (f : α ↪ β) (x y : α) :
Equiv.swap (f x) (f y) ∘ f = f ∘ Equiv.swap x y :=
f.injective.swap_comp x y