map_reindex — Mathlib

English

A symmetric version of the compatibility between map and reindexing.

Русский

Симметричная версия совместимости между map и переиндексацией.

LaTeX

$$$\\operatorname{map}_{e} \\circ (\\operatorname{reindex}_{s,e}) = (\\operatorname{reindex}_{t,e}) \\circ \\operatorname{map}_{e}$$$

Lean4

theorem map_reindex (f : Π i, s i →ₗ[R] t i) (e : ι ≃ ι₂) (x : ⨂[R] i, s i) :
    map (fun i ↦ f (e.symm i)) (reindex R s e x) = reindex R t e (map f x) :=
  DFunLike.congr_fun (map_comp_reindex_eq _ _) _

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