comap_reindex — Mathlib

English

Reindexing commutes with comap: applying reindex after comap f equals reindex after comap f on M.

Русский

Переиндексация и comap совместимы: применение переиндексации после comap f эквивалентно применению переиндексации после comap f к M.

LaTeX

$$$ (\\mathrm{reindex} g M).\\mathrm{comap} f = \\mathrm{reindex} g (M.\\mathrm{comap} f) $$$

Lean4

theorem comap_reindex (f : α' → α) (g : σ ≃ σ') : (reindex g M).comap f = reindex g (M.comap f) := by
  simp [comap, reindex]

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