Commit 2025-04-07 07:19 8b1673c7

feat(Geometry/Euclidean/Basic): projection of vertex to opposite face of simplex (#23712) Add two simple lemmas about the projection of a vertex of a simplex onto the opposite face (that arise while setting up the theory of incenter and excenter).

@[simp] lemma ne_orthogonalProjection_faceOpposite (i : Fin (n + 1)) : s.points i ≠
    orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) (s.points i) := by

lemma dist_orthogonalProjection_faceOpposite_pos (i : Fin (n + 1)) :
    0 < dist (s.points i)
      (orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) (s.points i)) := by