comp_swap_eq_update — Mathlib

English

For any f : α → β, the composition f ∘ swap i j equals update(update f j (f i)) i (f j).

Русский

Для любого f : α → β композиция f ∘ swap i j равна update(update f j (f i)) i (f j).

LaTeX

$$$f \circ \mathrm{swap}(i,j) = \mathrm{update}(\mathrm{update} f j (f i)) i (f j)$$$

Lean4

theorem comp_swap_eq_update (i j : α) (f : α → β) : f ∘ Equiv.swap i j = update (update f j (f i)) i (f j) := by
  rw [swap_eq_update, comp_update, comp_update, comp_id]

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