Centroid of a simplex in affine space

This file proves some basic properties of the centroid of a simplex in affine space. The definition of the centroid is based on Finset.univ.centroid applied to the set of vertices. For convenience, we use Simplex.centroid as an abbreviation.

This file also defines faceOppositeCentroid, which is the centroid of the facet of the simplex obtained by removing one vertex.

We prove several relations among the centroid, the faceOppositeCentroid, and the vertices of the simplex. In particular, we prove a version of Commandino's theorem in arbitrary dimensions: the centroid lies on each median, dividing it in a ratio of n : 1, where n is the dimension of the simplex.

Main definitions

• centroid is the centroid of a simplex, defined via Finset.univ.centroid on its vertices.

• faceOppositeCentroid is the centroid of the facet obtained by removing one vertex from the simplex.

• median is the line connecting a vertex to the corresponding faceOppositeCentroid.

References

• https://en.wikipedia.org/wiki/Median_(geometry)
• https://en.wikipedia.org/wiki/Commandino%27s_theorem

@[reducible, inline]

abbrev Affine.Simplex.centroid {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} (t : Simplex k P n) : P

The centroid of a simplex is the Finset.centroid of the set of all its vertices.

Equations

• t.centroid = Finset.centroid k Finset.univ t.points

theorem Affine.Simplex.univ_centroid_eq {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} (s : Simplex k P n) : Finset.centroid k Finset.univ s.points = s.centroid

theorem Affine.Simplex.centroid_mem_affineSpan {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] [CharZero k] {n : ℕ} (s : Simplex k P n) : s.centroid ∈ affineSpan k (Set.range s.points)

The centroid lines in the affine span of the simplex's vertices.

theorem Affine.Simplex.centroid_eq_affineCombination {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} (s : Simplex k P n) : s.centroid = (Finset.affineCombination k Finset.univ s.points) (Finset.centroidWeights k Finset.univ)

The centroid is equal to the affine combination of the points with centroidWeights.

theorem Affine.Simplex.centroid_notMem_affineSpan_of_ne_univ {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} [CharZero k] (s : Simplex k P n) {t : Set (Fin (n + 1))} (ht : t ≠ Set.univ) : s.centroid ∉ affineSpan k (s.points '' t)

The centroid of a simplex does not lie in the affine span of any proper subset of its vertices.

theorem Affine.Simplex.centroid_vsub_eq {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} [CharZero k] (s : Simplex k P n) (p : P) : s.centroid -ᵥ p = (↑n + 1)⁻¹ • ∑ x : Fin (n + 1), (s.points x -ᵥ p)

The vector from any point to the centroid is the average of vectors to the simplex vertices.

theorem Affine.Simplex.centroid_eq_smul_sum_vsub_vadd {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} [CharZero k] (s : Simplex k P n) (i : Fin (n + 1)) : s.centroid = (↑n + 1)⁻¹ • ∑ x : Fin (n + 1), (s.points x -ᵥ s.points i) +ᵥ s.points i

theorem Affine.Simplex.smul_centroid_vsub_point_eq_sum_vsub {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} [CharZero k] (s : Simplex k P n) (i : Fin (n + 1)) : (↑n + 1) • (s.centroid -ᵥ s.points i) = ∑ x : Fin (n + 1), (s.points x -ᵥ s.points i)

theorem Affine.Simplex.centroid_weighted_vsub_eq_zero {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} [CharZero k] (s : Simplex k P n) : ∑ i : Fin (n + 1), (s.points i -ᵥ s.centroid) = 0

The sum of vectors from the centroid to each vertex is zero.

theorem Affine.Simplex.eq_centroid_iff_sum_vsub_eq_zero {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} [CharZero k] {s : Simplex k P n} {p : P} : p = s.centroid ↔ ∑ i : Fin (n + 1), (s.points i -ᵥ p) = 0

A point is centroid if and only if the sum of vectors from the point to all vertices is zero.

theorem Affine.Simplex.face_centroid_eq_centroid {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} (s : Simplex k P n) {fs : Finset (Fin (n + 1))} {m : ℕ} (h : fs.card = m + 1) : Finset.centroid k Finset.univ (s.face h).points = Finset.centroid k fs s.points

The centroid of a face of a simplex as the centroid of a subset of the points.

@[simp]

theorem Affine.Simplex.centroid_eq_iff {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] [CharZero k] {n : ℕ} (s : Simplex k P n) {fs₁ fs₂ : Finset (Fin (n + 1))} {m₁ m₂ : ℕ} (h₁ : fs₁.card = m₁ + 1) (h₂ : fs₂.card = m₂ + 1) : Finset.centroid k fs₁ s.points = Finset.centroid k fs₂ s.points ↔ fs₁ = fs₂

Over a characteristic-zero division ring, the centroids given by two subsets of the points of a simplex are equal if and only if those faces are given by the same subset of points.

theorem Affine.Simplex.face_centroid_eq_iff {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] [CharZero k] {n : ℕ} (s : Simplex k P n) {fs₁ fs₂ : Finset (Fin (n + 1))} {m₁ m₂ : ℕ} (h₁ : fs₁.card = m₁ + 1) (h₂ : fs₂.card = m₂ + 1) : Finset.centroid k Finset.univ (s.face h₁).points = Finset.centroid k Finset.univ (s.face h₂).points ↔ fs₁ = fs₂

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 Affine.Simplex.centroid_eq_of_range_eq {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} {s₁ s₂ : Simplex k P n} (h : Set.range s₁.points = Set.range s₂.points) : Finset.centroid k Finset.univ s₁.points = Finset.centroid k Finset.univ s₂.points

Two simplices with the same points have the same centroid.

theorem Affine.Simplex.affineIndependent_points_update_centroid {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} [CharZero k] (s : Simplex k P n) (i : Fin (n + 1)) : AffineIndependent k (Function.update s.points i s.centroid)

Replacing a vertex of a simplex by its centroid preserves affine independence.

theorem Affine.Simplex.centroid_map {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] [CharZero k] {V₂ : Type u_4} {P₂ : Type u_5} [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] {n : ℕ} (s : Simplex k P n) (f : P →ᵃ[k] P₂) (hf : Function.Injective ⇑f) : (s.map f hf).centroid = f s.centroid

theorem Affine.Simplex.centroid_reindex {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {m n : ℕ} (s : Simplex k P m) (e : Fin (m + 1) ≃ Fin (n + 1)) : (s.reindex e).centroid = s.centroid

theorem Affine.Simplex.centroid_restrict {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] [CharZero k] {n : ℕ} (s : Simplex k P n) (S : AffineSubspace k P) (hS : affineSpan k (Set.range s.points) ≤ S) : ↑(s.restrict S hS).centroid = s.centroid

def Affine.Simplex.faceOppositeCentroid {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex k P n) (i : Fin (n + 1)) : P

The faceOppositeCentroid is the centroid of the face opposite to the vertex indexed by i.

Equations

• s.faceOppositeCentroid i = (s.faceOpposite i).centroid

theorem Affine.Simplex.faceOppositeCentroid_mem_affineSpan_face {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} [NeZero n] [CharZero k] (s : Simplex k P n) (i : Fin (n + 1)) : s.faceOppositeCentroid i ∈ affineSpan k (Set.range (s.faceOpposite i).points)

The centroid of the face opposite a vertex lies in the affine span of that face.

theorem Affine.Simplex.faceOppositeCentroid_eq_affineCombination {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex k P n) (i : Fin (n + 1)) : s.faceOppositeCentroid i = (Finset.affineCombination k {i}ᶜ s.points) fun (x : Fin (n + 1)) => (↑n)⁻¹

The faceOppositeCentroid is the affine combination of the complement vertices with equal weights 1/n.

theorem Affine.Simplex.faceOppositeCentroid_vsub_point_eq_smul_sum_vsub {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} [NeZero n] [CharZero k] (s : Simplex k P n) (i : Fin (n + 1)) : s.faceOppositeCentroid i -ᵥ s.points i = (↑n)⁻¹ • ∑ x : Fin (n + 1), (s.points x -ᵥ s.points i)

The vector from a vertex to the corresponding faceOppositeCentroid equals the average of the displacements to the other vertices.

theorem Affine.Simplex.faceOppositeCentroid_eq_sum_vsub_vadd {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} [NeZero n] [CharZero k] (s : Simplex k P n) (i : Fin (n + 1)) : s.faceOppositeCentroid i = (↑n)⁻¹ • ∑ x : Fin (n + 1), (s.points x -ᵥ s.points i) +ᵥ s.points i

The faceOppositeCentroid equals the average displacement from a vertex plus that vertex.

theorem Affine.Simplex.point_vsub_faceOppositeCentroid_eq_smul_sum_vsub {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} [NeZero n] [CharZero k] (s : Simplex k P n) (i : Fin (n + 1)) : s.points i -ᵥ s.faceOppositeCentroid i = (↑n)⁻¹ • ∑ x : Fin (n + 1), (s.points i -ᵥ s.points x)

The vector from a vertex to its faceOppositeCentroid equals the average of reversed displacements.

theorem Affine.Simplex.smul_faceOppositeCentroid_vsub_point_eq_sum_vsub {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} [NeZero n] [CharZero k] (s : Simplex k P n) (i : Fin (n + 1)) : ↑n • (s.faceOppositeCentroid i -ᵥ s.points i) = ∑ x : Fin (n + 1), (s.points x -ᵥ s.points i)

theorem Affine.Simplex.smul_centroid_vsub_point_eq_smul_faceOppositeCentroid_vsub_point {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} [NeZero n] [CharZero k] (s : Simplex k P n) (i : Fin (n + 1)) : (↑n + 1) • (s.centroid -ᵥ s.points i) = ↑n • (s.faceOppositeCentroid i -ᵥ s.points i)

theorem Affine.Simplex.faceOppositeCentroid_vsub_faceOppositeCentroid {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} [NeZero n] [CharZero k] (s : Simplex k P n) (i j : Fin (n + 1)) : s.faceOppositeCentroid i -ᵥ s.faceOppositeCentroid j = (↑n)⁻¹ • (s.points j -ᵥ s.points i)

The vector between two faceOppositeCentroid equals n⁻¹ times the vector between the corresponding vertices.

theorem Affine.Simplex.faceOppositeCentroid_vsub_point_eq_smul_vsub {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} [NeZero n] [CharZero k] (s : Simplex k P n) (i : Fin (n + 1)) : s.faceOppositeCentroid i -ᵥ s.points i = (↑n + 1) • (s.faceOppositeCentroid i -ᵥ s.centroid)

The vector from a vertex to its faceOppositeCentroid is (n+1) times the vector from the centroid to that faceOppositeCentroid.

theorem Affine.Simplex.point_vsub_faceOppositeCentroid_eq_smul_vsub {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} [NeZero n] [CharZero k] (s : Simplex k P n) (i : Fin (n + 1)) : s.points i -ᵥ s.faceOppositeCentroid i = (↑n + 1) • (s.centroid -ᵥ s.faceOppositeCentroid i)

theorem Affine.Simplex.point_vsub_centroid_eq_smul_vsub {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} [NeZero n] [CharZero k] (s : Simplex k P n) (i : Fin (n + 1)) : s.points i -ᵥ s.centroid = ↑n • (s.centroid -ᵥ s.faceOppositeCentroid i)

Commandino's theorem : For n-simplex, the vector from a vertex to the centroid equals n times the vector from the centroid to the corresponding faceOppositeCentroid.

theorem Affine.Simplex.centroid_vsub_point_eq_smul_vsub {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} [NeZero n] [CharZero k] (s : Simplex k P n) (i : Fin (n + 1)) : s.centroid -ᵥ s.points i = ↑n • (s.faceOppositeCentroid i -ᵥ s.centroid)

Reverse version of point_vsub_centroid_eq_smul_vsub.

theorem Affine.Simplex.faceOppositeCentroid_vsub_centroid_eq_smul_vsub {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} [NeZero n] [CharZero k] (s : Simplex k P n) (i : Fin (n + 1)) : s.faceOppositeCentroid i -ᵥ s.centroid = (↑n)⁻¹ • (s.centroid -ᵥ s.points i)

The vector from centroid to a vertex corresponding faceOppositeCentroid is n⁻¹ of the vector from the vertex to the centroid.

theorem Affine.Simplex.centroid_vsub_faceOppositeCentroid_eq_smul_vsub {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} [NeZero n] [CharZero k] (s : Simplex k P n) (i : Fin (n + 1)) : s.centroid -ᵥ s.faceOppositeCentroid i = (↑n)⁻¹ • (s.points i -ᵥ s.centroid)

Reverse version of faceOppositeCentroid_vsub_centroid_eq_smul_vsub

theorem Affine.Simplex.centroid_eq_smul_vsub_vadd_point {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} [NeZero n] [CharZero k] (s : Simplex k P n) (i : Fin (n + 1)) : s.centroid = ↑n • (s.faceOppositeCentroid i -ᵥ s.centroid) +ᵥ s.points i

The centroid of an n-simplex can be obtained from a vertex by adding n times the vector from the centroid to the faceOppositeCentroid.

theorem Affine.Simplex.faceOppositeCentroid_eq_smul_vsub_vadd_point {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} [NeZero n] [CharZero k] (s : Simplex k P n) (i : Fin (n + 1)) : s.faceOppositeCentroid i = (↑n)⁻¹ • (s.centroid -ᵥ s.points i) +ᵥ s.centroid

The point faceOppositeCentroid of an n-simplex can be obtained from the centroid by adding n⁻¹ times the vector from the vertex to the centroid.

@[simp]

theorem Affine.Simplex.faceOppositeCentroid_map {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] [CharZero k] {V₂ : Type u_4} {P₂ : Type u_5} [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] {n : ℕ} [NeZero n] (s : Simplex k P n) (f : P →ᵃ[k] P₂) (hf : Function.Injective ⇑f) {i : Fin (n + 1)} : (s.map f hf).faceOppositeCentroid i = f (s.faceOppositeCentroid i)

@[simp]

theorem Affine.Simplex.faceOppositeCentroid_restrict {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} [NeZero n] [CharZero k] (s : Simplex k P n) (S : AffineSubspace k P) (hS : affineSpan k (Set.range s.points) ≤ S) {i : Fin (n + 1)} : ↑((s.restrict S hS).faceOppositeCentroid i) = s.faceOppositeCentroid i

@[simp]

theorem Affine.Simplex.faceOppositeCentroid_reindex {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {m n : ℕ} [NeZero m] [NeZero n] (s : Simplex k P m) (e : Fin (m + 1) ≃ Fin (n + 1)) : (s.reindex e).faceOppositeCentroid = s.faceOppositeCentroid ∘ ⇑e.symm

def Affine.Simplex.median {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex k P n) (i : Fin (n + 1)) : AffineSubspace k P

The median of a simplex is the line through a vertex and its corresponding faceOppositeCentroid.

Equations

• s.median i = affineSpan k {s.points i, s.faceOppositeCentroid i}

@[simp]

theorem Affine.Simplex.median_reindex {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {m n : ℕ} [NeZero m] [NeZero n] (s : Simplex k P n) (e : Fin (n + 1) ≃ Fin (m + 1)) : (s.reindex e).median = s.median ∘ ⇑e.symm

@[simp]

theorem Affine.Simplex.median_map {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] [CharZero k] {V₂ : Type u_4} {P₂ : Type u_5} [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] {n : ℕ} [NeZero n] (s : Simplex k P n) (i : Fin (n + 1)) (f : P →ᵃ[k] P₂) (hf : Function.Injective ⇑f) : (s.map f hf).median i = AffineSubspace.map f (s.median i)

theorem Affine.Simplex.median_restrict {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} [NeZero n] [CharZero k] (s : Simplex k P n) (i : Fin (n + 1)) (S : AffineSubspace k P) (hS : affineSpan k (Set.range s.points) ≤ S) : AffineSubspace.map S.subtype ((s.restrict S hS).median i) = s.median i

theorem Affine.Simplex.faceOppositeCentroid_mem_median {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex k P n) (i : Fin (n + 1)) : s.faceOppositeCentroid i ∈ s.median i

The faceOppositeCentroid lines on the median through the corresponding vertex.

theorem Affine.Simplex.point_mem_median {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex k P n) (i : Fin (n + 1)) : s.points i ∈ s.median i

A vertex lies on its median.

theorem Affine.Simplex.centroid_mem_median {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} [NeZero n] [CharZero k] (s : Simplex k P n) (i : Fin (n + 1)) : s.centroid ∈ s.median i

The centroid lies on the median from any vertex.

theorem Affine.Simplex.median_eq_line_point_centroid {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} [NeZero n] [CharZero k] (s : Simplex k P n) (i : Fin (n + 1)) : s.median i = affineSpan k {s.points i, s.centroid}

The median of a simplex is the line through the vertex and the centroid.

theorem Affine.Simplex.eq_centroid_of_forall_mem_median {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} [NeZero n] [CharZero k] (s : Simplex k P n) {hn : 1 < n} {p : P} (h : ∀ (i : Fin (n + 1)), p ∈ s.median i) : p = s.centroid

The medians of a simplex are concurrent at its centroid.