reindex_symm_reindex — Mathlib

English

Reindexing a simplex by an equivalence does not change the set of its vertex positions; it just reorders them.

Русский

Перестановка индексов симплекса не изменяет множество его вершин, а лишь упорядочивает их.

LaTeX

$$$\\mathrm{Set.range}(s.reindex e).points = \\mathrm{Set.range}(s).points$$$

Lean4

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

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