Theorem Convexity.StdSimplex.topologicalSpaceInduced.continuous_map

Modification history

2026-08-11 15:45
Mathlib/Geometry/Convex/ConvexSpace/Topology.lean
feat(Geometry/Convex): a topology on StdSimplex (#42131) …
Added Convexity.StdSimplex.topologicalSpaceInduced.continuous_mapView on Github →