swap_comp — Mathlib

English

For a left-to-right composition with swap and an injective f, we have f ∘ swap = swap ∘ f, i.e., swap (f x) (f y) ∘ f = f ∘ swap x y.

Русский

При инъекции f имеем: f ∘ swap = swap ∘ f, то есть swap (f x) (f y) ∘ f = f ∘ swap x y.

LaTeX

$$$\\text{swap} (f x) (f y) \\circ f = f \\circ \\text{swap} x y.$$$

Lean4

theorem swap_comp [DecidableEq α] [DecidableEq β] {f : α → β} (hf : Function.Injective f) (x y : α) :
    Equiv.swap (f x) (f y) ∘ f = f ∘ Equiv.swap x y :=
  funext fun _ => hf.swap_apply _ _ _

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