swap_apply_def — Mathlib

English

The action of swap on x is given by a simple conditional: swap(a,b)(x) = if x = a then b else if x = b then a else x.

Русский

Действие swap на x задаётся условием: swap(a,b)(x) = если x = a, то b; иначе если x = b, то a; иначе x.

LaTeX

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

Lean4

theorem swap_apply_def (a b x : α) : swap a b x = if x = a then b else if x = b then a else x :=
  rfl

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