Centroid of a simplex in affine space #
This file proves some basic properties of the centroid of a simplex in affine space.
@[simp]
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)
:
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)
:
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)
:
Two simplices with the same points have the same centroid.