reindex_tprod — Mathlib

English

Reindexing a tprod along e distributes the indices, giving the tprod of the pulled-back family.

Русский

Переиндексация tprod по e распаковывает индексы и даёт tprod от возвращённой, вытянутой по обратному отображению семье.

LaTeX

$$$\\operatorname{reindex}_{R,s,e}\\bigl(\\operatorname{tprod}_R f\\bigr) = \\operatorname{tprod}_R \\bigl(\\lambda i. f(e^{-1}(i))\\bigr).$$$

Lean4

@[simp]
theorem reindex_tprod (e : ι ≃ ι₂) (f : Π i, s i) : reindex R s e (tprod R f) = tprod R fun i ↦ f (e.symm i) :=
  by
  dsimp [reindex]
  exact liftAux_tprod _ f

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