swap — Mathlib

English

Define swap(a,b) as the permutation that transposes a and b and fixes all other elements.

Русский

Определим swap(a,b) как перестановку, которая меняет местами a и b и фиксирует все остальные элементы.

LaTeX

$$$\\text{swap}(a,b)=\\langle\\text{swapCore}(a,b), \\text{swapCore}(a,b),\\dots\\rangle$$$

Lean4

/-- `swap a b` is the permutation that swaps `a` and `b` and
  leaves other values as is. -/
def swap (a b : α) : Perm α :=
  ⟨swapCore a b, swapCore a b, fun r => swapCore_swapCore r a b, fun r => swapCore_swapCore r a b⟩

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