Commit 2026-08-11 15:45 5e3076d0

feat(Geometry/Convex): a topology on StdSimplex (#42131) In this PR, we define a topology on the standard simplex StdSimplex R M. When M is finite, this is the topology that is induced by the embedding StdSimplex R M → (M → R). In general, we use the supremum of the coinduced topologies for the maps StdSimplex.map f : StdSimplex R ι → StdSimplex R M where f : ι → M is a map from a finite set ι.