IsSwap — Mathlib

English

A permutation is a transposition if it swaps two elements and fixes all others.

Русский

Перестановка является транспозицией, если она меняет две элемента местами и фиксирует все остальные.

LaTeX

$$$$ \text{IsSwap}(f) \iff \exists x\exists y\ (x\neq y \wedge f = \mathrm{swap}(x,y)). $$$$

Lean4

/-- `f.IsSwap` indicates that the permutation `f` is a transposition of two elements. -/
def IsSwap (f : Perm α) : Prop :=
  ∃ x y, x ≠ y ∧ f = swap x y

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