reindex_reindex_symm — Mathlib

English

Reindexing by the inverse equivalence then by the equivalence returns to the original simplex.

Русский

Перестановка индексов по обратной эквивалентности затем по самой эквивалентности возвращает исходный симплекс.

LaTeX

$$(s.reindex e.symm).reindex e = s$$

Lean4

/-- Reindexing by an equivalence and its inverse yields the original simplex. -/
@[simp]
theorem reindex_reindex_symm {m n : ℕ} (s : Simplex k P m) (e : Fin (m + 1) ≃ Fin (n + 1)) :
    (s.reindex e).reindex e.symm = s := by rw [← reindex_trans, Equiv.self_trans_symm, reindex_refl]

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