Documentation

Mathlib.Geometry.Euclidean.Simplex

Simplices in Euclidean spaces. #

This file defines properties of simplices in a Euclidean space.

Main definitions #

source
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
source
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
Instances For
    source
    @[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
    source
    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
    source
    theorem Affine.Simplex.dist_point_centroid {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (i : Fin (n + 1)) :
    dist (s.points i) s.centroid = ↑n * dist s.centroid (s.faceOppositeCentroid i)

    The distance from a vertex to the centroid equals n times the distance from the centroid to the corresponding faceOppositeCentroid.

    source
    theorem Affine.Simplex.dist_point_faceOppositeCentroid {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (i : Fin (n + 1)) :
    dist (s.points i) (s.faceOppositeCentroid i) = (↑n + 1) * dist s.centroid (s.faceOppositeCentroid i)

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

    source
    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
    source
    theorem Affine.Triangle.dist_point_centroid {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Triangle ℝ P) (i : Fin 3) :
    dist (t.points i) (Simplex.centroid t) = 2 * dist (Simplex.centroid t) (Simplex.faceOppositeCentroid t i)

    In a triangle, the distance from a vertex to the centroid equals twice the distance from the centroid to the faceOppositeCentroid.

    source
    theorem Affine.Triangle.dist_point_faceOppositeCentroid {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Triangle ℝ P) (i : Fin 3) :
    dist (t.points i) (Simplex.faceOppositeCentroid t i) = 3 * dist (Simplex.centroid t) (Simplex.faceOppositeCentroid t i)

    In a triangle, the distance from a vertex to the faceOppositeCentroid equals three times the distance from the centroid to the faceOppositeCentroid.