swap_comp_apply — Mathlib

English

For any π ∈ Perm α, the composite π ∘ swap a b acts as: it sends x to b if π(x)=a, to a if π(x)=b, and to π(x) otherwise.

Русский

Для любой-перестановки π из α, составной функция π ∘ swap(a,b) отправляет x в b если π(x)=a, в a если π(x)=b, иначе в π(x).

LaTeX

$$$(\pi \circ \mathrm{swap}(a,b))(x) = \begin{cases} b, & \pi(x)=a \\ a, & \pi(x)=b \\ \pi(x), & \text{иначе} \end{cases}$$$

Lean4

theorem swap_comp_apply {a b x : α} (π : Perm α) :
    π.trans (swap a b) x = if π x = a then b else if π x = b then a else π x :=
  by
  cases π
  rfl

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