Simplices in Euclidean spaces.

This file defines properties of simplices in a Euclidean space.

Main definitions

• Affine.Simplex.AcuteAngled

theorem Affine.Simplex.Equilateral.angle_eq_pi_div_three {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} {s : Simplex ℝ P n} (he : s.Equilateral) {i₁ i₂ i₃ : Fin (n + 1)} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : EuclideanGeometry.angle (s.points i₁) (s.points i₂) (s.points i₃) = Real.pi / 3

def Affine.Simplex.AcuteAngled {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Simplex ℝ P n) : Prop

The property of all angles of a simplex being acute.

Equations

• s.AcuteAngled = ∀ (i₁ i₂ i₃ : Fin (n + 1)), i₁ ≠ i₂ → i₁ ≠ i₃ → i₂ ≠ i₃ → EuclideanGeometry.angle (s.points i₁) (s.points i₂) (s.points i₃) < Real.pi / 2

@[simp]

theorem Affine.Simplex.acuteAngled_reindex_iff {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {m n : ℕ} {s : Simplex ℝ P m} (e : Fin (m + 1) ≃ Fin (n + 1)) : (s.reindex e).AcuteAngled ↔ s.AcuteAngled

theorem Affine.Simplex.Equilateral.acuteAngled {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} {s : Simplex ℝ P n} (he : s.Equilateral) : s.AcuteAngled

theorem Affine.Triangle.acuteAngled_iff_angle_lt {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {t : Triangle ℝ P} : Simplex.AcuteAngled t ↔ EuclideanGeometry.angle (t.points 0) (t.points 1) (t.points 2) < Real.pi / 2 ∧ EuclideanGeometry.angle (t.points 1) (t.points 2) (t.points 0) < Real.pi / 2 ∧ EuclideanGeometry.angle (t.points 2) (t.points 0) (t.points 1) < Real.pi / 2