swap_apply — Mathlib

English

If f is injective, then swapping the outputs of f on x, y, z is the same as applying f to the swapped inputs: Equiv.swap (f x) (f y) (f z) = f (Equiv.swap x y z).

Русский

Пусть f — инъективная функция. Тогда замена аргументов через swap удовлетворяет равенству: Equiv.swap (f x) (f y) (f z) = f (Equiv.swap x y z).

LaTeX

$$$\\mathrm{swap}(f x)(f y)(f z) = f(\\mathrm{swap}(x,y,z)).$$$

Lean4

theorem swap_apply [DecidableEq α] [DecidableEq β] {f : α → β} (hf : Function.Injective f) (x y z : α) :
    Equiv.swap (f x) (f y) (f z) = f (Equiv.swap x y z) :=
  Eq.symm (map_swap hf x y z)

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