reindex_range_points — Mathlib

English

Reindexing by the identity equivalence yields the original simplex (redundant restatement).

Русский

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

LaTeX

$$$s.reindex(\\mathrm{Equiv.refl}(\\mathrm{Fin}(n+1))) = s$$$

Lean4

/-- Reindexing a simplex produces one with the same set of points. -/
@[simp]
theorem reindex_range_points {m n : ℕ} (s : Simplex k P m) (e : Fin (m + 1) ≃ Fin (n + 1)) :
    Set.range (s.reindex e).points = Set.range s.points := by
  rw [reindex, Set.range_comp, Equiv.range_eq_univ, Set.image_univ]

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