swap_swap — Mathlib

English

Swapping β and γ twice returns the original kernel: (swap β γ) ∘ₖ (swap γ β) = Kernel.id.

Русский

Двойной обмен местами β и γ возвращает исходное ядро: (swap β γ) ∘ₖ (swap γ β) = Kernel.id.

LaTeX

$$$ (\text{swap } β γ) \circ_K (\text{swap } γ β) = \text{Kernel.id}$$$

Lean4

@[simp]
theorem swap_swap : (swap α β) ∘ₖ (swap β α) = Kernel.id := by
  simp_rw [swap, Kernel.deterministic_comp_deterministic, Prod.swap_swap_eq, Kernel.id]

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