Simplices in torsors over normed spaces.

This file defines properties of simplices in a NormedAddTorsor.

Main definitions

• Affine.Simplex.Scalene
• Affine.Simplex.Equilateral
• Affine.Simplex.Regular

def Affine.Simplex.Scalene {R : Type u_1} {V : Type u_2} {P : Type u_3} [Ring R] [SeminormedAddCommGroup V] [PseudoMetricSpace P] [Module R V] [NormedAddTorsor V P] {n : ℕ} (s : Simplex R P n) : Prop

A simplex is scalene if all the edge lengths are different.

theorem Affine.Simplex.Scalene.dist_ne {R : Type u_1} {V : Type u_2} {P : Type u_3} [Ring R] [SeminormedAddCommGroup V] [PseudoMetricSpace P] [Module R V] [NormedAddTorsor V P] {n : ℕ} {s : Simplex R P n} (hs : s.Scalene) {i₁ i₂ i₃ i₄ : Fin (n + 1)} (h₁₂ : i₁ ≠ i₂) (h₃₄ : i₃ ≠ i₄) (h₁₂₃₄ : ¬(i₁ = i₃ ∧ i₂ = i₄)) (h₁₂₄₃ : ¬(i₁ = i₄ ∧ i₂ = i₃)) : dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)

@[simp]

theorem Affine.Simplex.scalene_reindex_iff {R : Type u_1} {V : Type u_2} {P : Type u_3} [Ring R] [SeminormedAddCommGroup V] [PseudoMetricSpace P] [Module R V] [NormedAddTorsor V P] {m n : ℕ} {s : Simplex R P m} (e : Fin (m + 1) ≃ Fin (n + 1)) : (s.reindex e).Scalene ↔ s.Scalene

def Affine.Simplex.Equilateral {R : Type u_1} {V : Type u_2} {P : Type u_3} [Ring R] [SeminormedAddCommGroup V] [PseudoMetricSpace P] [Module R V] [NormedAddTorsor V P] {n : ℕ} (s : Simplex R P n) : Prop

A simplex is equilateral if all the edge lengths are equal.

theorem Affine.Simplex.Equilateral.dist_eq {R : Type u_1} {V : Type u_2} {P : Type u_3} [Ring R] [SeminormedAddCommGroup V] [PseudoMetricSpace P] [Module R V] [NormedAddTorsor V P] {n : ℕ} {s : Simplex R P n} (he : s.Equilateral) {i₁ i₂ i₃ i₄ : Fin (n + 1)} (h₁₂ : i₁ ≠ i₂) (h₃₄ : i₃ ≠ i₄) : dist (s.points i₁) (s.points i₂) = dist (s.points i₃) (s.points i₄)

@[simp]

theorem Affine.Simplex.equilateral_reindex_iff {R : Type u_1} {V : Type u_2} {P : Type u_3} [Ring R] [SeminormedAddCommGroup V] [PseudoMetricSpace P] [Module R V] [NormedAddTorsor V P] {m n : ℕ} {s : Simplex R P m} (e : Fin (m + 1) ≃ Fin (n + 1)) : (s.reindex e).Equilateral ↔ s.Equilateral

def Affine.Simplex.Regular {R : Type u_1} {V : Type u_2} {P : Type u_3} [Ring R] [SeminormedAddCommGroup V] [PseudoMetricSpace P] [Module R V] [NormedAddTorsor V P] {n : ℕ} (s : Simplex R P n) : Prop

A simplex is regular if it is equivalent under an isometry to any reindexing.

@[simp]

theorem Affine.Simplex.regular_reindex_iff {R : Type u_1} {V : Type u_2} {P : Type u_3} [Ring R] [SeminormedAddCommGroup V] [PseudoMetricSpace P] [Module R V] [NormedAddTorsor V P] {m n : ℕ} {s : Simplex R P m} (e : Fin (m + 1) ≃ Fin (n + 1)) : (s.reindex e).Regular ↔ s.Regular

theorem Affine.Simplex.Regular.equilateral {R : Type u_1} {V : Type u_2} {P : Type u_3} [Ring R] [SeminormedAddCommGroup V] [PseudoMetricSpace P] [Module R V] [NormedAddTorsor V P] {n : ℕ} {s : Simplex R P n} (hr : s.Regular) : s.Equilateral

theorem Affine.Triangle.scalene_iff_dist_ne_and_dist_ne_and_dist_ne {R : Type u_1} {V : Type u_2} {P : Type u_3} [Ring R] [SeminormedAddCommGroup V] [PseudoMetricSpace P] [Module R V] [NormedAddTorsor V P] {t : Triangle R P} : Simplex.Scalene t ↔ dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2) ∧ dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2) ∧ dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)

theorem Affine.Triangle.equilateral_iff_dist_eq_and_dist_eq {R : Type u_1} {V : Type u_2} {P : Type u_3} [Ring R] [SeminormedAddCommGroup V] [PseudoMetricSpace P] [Module R V] [NormedAddTorsor V P] {t : Triangle R P} {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : Simplex.Equilateral t ↔ dist (t.points i₁) (t.points i₂) = dist (t.points i₁) (t.points i₃) ∧ dist (t.points i₁) (t.points i₂) = dist (t.points i₂) (t.points i₃)

theorem Affine.Triangle.equilateral_iff_dist_01_eq_02_and_dist_01_eq_12 {R : Type u_1} {V : Type u_2} {P : Type u_3} [Ring R] [SeminormedAddCommGroup V] [PseudoMetricSpace P] [Module R V] [NormedAddTorsor V P] {t : Triangle R P} : Simplex.Equilateral t ↔ dist (t.points 0) (t.points 1) = dist (t.points 0) (t.points 2) ∧ dist (t.points 0) (t.points 1) = dist (t.points 1) (t.points 2)