map_swap_eq_comap_swap — Mathlib

English

A specific equality saying that a nested swap-based map equals a corresponding comap with another swap.

Русский

Специфическое равенство, показывающее, что вложенное преобразование swap эквивалентно некоторому comap с другим swap.

LaTeX

$$map (fun p : (α × β) × γ × δ => ((p.1.1, p.2.1), (p.1.2, p.2.2))) f = comap (fun p : (α × γ) × β × δ => ((p.1.1, p.2.1), (p.1.2, p.2.2))) f$$

Lean4

theorem map_swap_eq_comap_swap {f : Filter (α × β)} : map Prod.swap f = comap Prod.swap f :=
  map_eq_comap_of_inverse Prod.swap_swap_eq Prod.swap_swap_eq

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