swap_apply — Mathlib

English

The map swap applied to p is the same as evaluating p by swapping the variables, i.e., swap(p) = p.aevalAeval (A := R[X][Y]) Y (C X).

Русский

Применение swap к p равно вычислению p после обмена переменных; swap(p) = p.aevalAeval (A := R[X][Y]) Y (C X).

LaTeX

$$$swap(p) = p.aevalAeval (A := R[X][Y])\\; Y\\; (C X).$$$

Lean4

@[simp]
theorem swap_apply (p : R[X][Y]) : swap p = p.aevalAeval (A := R[X][Y]) Y (C X) :=
  rfl

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