English
If two simplices have the same set of vertex points, then their centroids agree.
Русский
Если два симплекса имеют один и тот же набор вершин, то их центроиды совпадают.
LaTeX
$$$\operatorname{Set.range}(s_1.points) = \operatorname{Set.range}(s_2.points) \Rightarrow \operatorname{Finset.univ.centroid}\ k\ s_1.points = \operatorname{Finset.univ.centroid}\ k\ s_2.points$$$
Lean4
/-- Two simplices with the same points have the same centroid. -/
theorem centroid_eq_of_range_eq {n : ℕ} {s₁ s₂ : Simplex k P n} (h : Set.range s₁.points = Set.range s₂.points) :
Finset.univ.centroid k s₁.points = Finset.univ.centroid k s₂.points :=
by
rw [← Set.image_univ, ← Set.image_univ, ← Finset.coe_univ] at h
exact
Finset.univ.centroid_eq_of_inj_on_of_image_eq k _ (fun _ _ _ _ he => AffineIndependent.injective s₁.independent he)
(fun _ _ _ _ he => AffineIndependent.injective s₂.independent he) h
