reindex_trans — Mathlib

English

Reindexing by the composition of two equivalences equals reindexing twice in succession.

Русский

Перестановка индексов по композиции двух эквивалентностей равна последовательной перестановке дважды.

LaTeX

$$$s.reindex(e_1\\!\\,\\!\\!\\!\\!\\!\\!\\!\\!\\.trans e_2) = (s.reindex e_1).reindex e_2$$$

Lean4

/-- Reindexing by the composition of two equivalences is the same as reindexing twice. -/
@[simp]
theorem reindex_trans {n₁ n₂ n₃ : ℕ} (e₁₂ : Fin (n₁ + 1) ≃ Fin (n₂ + 1)) (e₂₃ : Fin (n₂ + 1) ≃ Fin (n₃ + 1))
    (s : Simplex k P n₁) : s.reindex (e₁₂.trans e₂₃) = (s.reindex e₁₂).reindex e₂₃ :=
  rfl

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