circumsphere_reindex — Mathlib

English

Same as circumsphere_reindex; relabeling vertices does not affect circumsphere.

Русский

Переиндексирование вершин не влияет на circumsphere.

LaTeX

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

Lean4

/-- Reindexing a simplex along an `Equiv` of index types does not change the circumsphere. -/
@[simp]
theorem circumsphere_reindex {m n : ℕ} (s : Simplex ℝ P m) (e : Fin (m + 1) ≃ Fin (n + 1)) :
    (s.reindex e).circumsphere = s.circumsphere :=
  by
  refine s.circumsphere_unique_dist_eq.2 _ ⟨?_, ?_⟩ <;> rw [← s.reindex_range_points e]
  · exact (s.reindex e).circumsphere_unique_dist_eq.1.1
  · exact (s.reindex e).circumsphere_unique_dist_eq.1.2

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