swap_map — Mathlib

English

For f: α → α and g: β → β, swap semiconjugates the product map: swap ∘ Prod.map f g = Prod.map g f ∘ swap.

Русский

Для f: α→α и g: β→β, swap полуподчиняет отображение: swap ∘ Prod.map f g = Prod.map g f ∘ swap.

LaTeX

$$$\\\\operatorname{swap} \\\\\\circ \\\\operatorname{Prod.map} f g = \\\\operatorname{Prod.map} g f \\\\circ \\\\operatorname{swap}.$$$

Lean4

theorem _root_.Function.Semiconj.swap_map (f : α → α) (g : β → β) : Function.Semiconj swap (map f g) (map g f) :=
  Function.semiconj_iff_comp_eq.2 (map_comp_swap g f).symm

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