Naming of `Simplex.points`

Stream: mathlib4

[Jovan Gerbscheid]

I don't like the name Affine.Simplex.points, because in practice this means that to refer to vertex i of a simplex s, we write s.points i. And I get really confused by the plural points. (Compare Affine.Simplex.faceOpposite, which isn't called facesOpposite). I think this should be renamed to point or vertex. And points or vertices could be defined as s.points : Set P := Set.range s.point.

[Jovan Gerbscheid]

An orthogonal quesiton is why we use points instead of the more common vertices.

[Joseph Myers]

Whatever you call it, having a coercion to function would allow you to write s i and use the name a lot less.

I suspect the affine span of the set of vertices is used a lot more than the set of vertices is used directly (and so has a stronger case for having its own definition and associated API for that definition).

[Eric Wieser]

I agree that singular would be clearer here