swap_map — Mathlib

English

Applying swap after mapping is the same as mapping after swapping: swap M' N' (map f g x) = map g f (swap M N x).

Русский

Применение swap после отображения равно отображению после swap: swap M' N'(map f g x) = map g f (swap M N x).

LaTeX

$$$ \mathrm{swap}_{M',N'}( \mathrm{map}(f,g)(x) ) = \mathrm{map}(g,f)( \mathrm{swap}_{M,N}(x) ) $$$

Lean4

@[to_additive]
theorem swap_map (f : M →* M') (g : N →* N') (x : M ∗ N) : swap M' N' (map f g x) = map g f (swap M N x) :=
  DFunLike.congr_fun (swap_comp_map f g) x

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