swap_comp — Mathlib

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

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