swapLeft_apply — Mathlib

English

Applying swapLeft to a kernel at an input a gives the same as evaluating the original kernel at the swapped input.

Русский

Применяя swapLeft к ядру в точке a, получаем то же самое, что и применение исходного ядра к swapped входу.

LaTeX

$$$\text{swapLeft}(\kappa)\; a = \kappa\; a^{\mathrm{swap}}$$$

Lean4

@[simp]
theorem swapLeft_apply (κ : Kernel (α × β) γ) (a : β × α) : swapLeft κ a = κ a.swap :=
  rfl

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