map_reindex_symm — Mathlib

English

A symmetry version of map commuting with the inverse reindex.

Русский

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

LaTeX

$$$\\operatorname{map} \\circ (\\operatorname{reindex}_{s,e}).\\mathrm{symm} = (\\operatorname{reindex}_{t,e}).\\mathrm{symm} \\circ \\operatorname{map} (\\lambda i. f(e^{-1}(i)))$$$

Lean4

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

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