Commit 2025-03-13 08:51 ea606a7f

feat(LinearAlgebra/AffineSpace/Independent): interior of a simplex (#21929) Define the notion of the interior of a simplex (Affine.Simplex.interior), and also the corresponding closed set (Affine.Simplex.closedInterior). It's common in geometry to refer to a point being in the interior of a triangle, and having such a definition allows such a statement to be made without depending on the convexity refactor. Furthermore, this is a common enough concept that I think it makes sense for it to have its own definition and API even in the presence of the convexity refactor; intrinsicInterior k (convexHull k (Set.range s.points)) is not exactly a convenient way to refer to this common construct. (The convexity refactor would of course allow the equivalence of the two definitions to be stated and proved, or the definitions here could be redefined in terms of the general convexity ones at that point if desired.) There are plenty of things that could be stated and proved using this definition (e.g. conditions for triangle centers to be inside the triangle) though this PR doesn't do anything like that beyond one API lemma saying when an affine combination lies in the interior of a simplex. The corresponding closedInterior is by analogy to how, for example, we have both ball and closedBall in metric spaces. The definitions are also intended to be analogous to such definitions for (not necessarily convex) polygons once we have those defined: sometimes when considering a polygon as a set of points in a plane you want the interior as an open set, sometimes the interior together with the boundary (and this analogy with polygons that aren't necessarily convex is why a simpler name such as Affine.Simplex.convexHull wasn't used for closedInterior).