English
Over a characteristic-zero division ring, the centroids of two faces of a simplex are equal if and only if those faces correspond to the same subset of vertices.
Русский
В характеристики ноль поля деления кольца k центроиды двух граней симплекса равны тогда и только тогда, когда эти грани соответствуют одному и тому же подмножеству вершин.
LaTeX
$$$ \operatorname{Finset.univ.centroid}\ k\ (s.face h_1).points = \operatorname{Finset.univ.centroid}\ k\ (s.face h_2).points \iff fs_1 = fs_2$$$
Lean4
/-- Over a characteristic-zero division ring, the centroids of two
faces of a simplex are equal if and only if those faces are given by
the same subset of points. -/
theorem face_centroid_eq_iff [CharZero k] {n : ℕ} (s : Simplex k P n) {fs₁ fs₂ : Finset (Fin (n + 1))} {m₁ m₂ : ℕ}
(h₁ : #fs₁ = m₁ + 1) (h₂ : #fs₂ = m₂ + 1) :
Finset.univ.centroid k (s.face h₁).points = Finset.univ.centroid k (s.face h₂).points ↔ fs₁ = fs₂ :=
by
rw [face_centroid_eq_centroid, face_centroid_eq_centroid]
exact s.centroid_eq_iff h₁ h₂
